Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Command line option to return configuration data #362

Open
MSoegtropIMC opened this issue Jun 29, 2020 · 3 comments
Open

Command line option to return configuration data #362

MSoegtropIMC opened this issue Jun 29, 2020 · 3 comments

Comments

@MSoegtropIMC
Copy link
Contributor

For multi platform installations of CompCert (see e.g. coq/opam#1319) it would be good to have a command line option to return the configuration of ccomp and clightgen. This makes it easier to check e.g. in makefiles if the supplied binary has the right architecture.

Currently this is solved in opam by installing non default compcert into a non default root, so that one can derive the config file path from the binary path, but this is not very generic and also a bit fragile.

An alternative (or additional) approach would be to have standard prefixes for architectures, e.g. as typically done for cross gcc.

@xavierleroy
Copy link
Contributor

There's already much configuration information available in the compcert.ini file, installed in .../share/compcert.ini, and in the compcert.config file, installed (at your recent request) in .../lib/compcert/coq/compcert.config. Do we really need a third way to access this information?

@MSoegtropIMC
Copy link
Contributor Author

The issue is that if you have several compcert variants installed and get a compcert or clightgen binary say via an evironment variable in a make file, it is hard to tell to which of the several compcert.config file this binary belongs to. The only way I see to figure this is out is look at the path of the binary and have some conventions to transform the path of a binary to the path of a config file or to rely on that both paths are configured separately and consistently.

One option would be, if ccomp and clightgen would have a way to return the full path of the corresponding configuration file which belongs to them.

@xavierleroy
Copy link
Contributor

Related to #386

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants