Repository navigation
Command line option to return configuration data #362
Description
For multi platform installations of CompCert (see e.g. rocq-prover/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.
Activity
xavierleroy commentedon Jul 7, 2020
There's already much configuration information available in the
compcert.inifile, installed in.../share/compcert.ini, and in thecompcert.configfile, installed (at your recent request) in.../lib/compcert/coq/compcert.config. Do we really need a third way to access this information?MSoegtropIMC commentedon Jul 7, 2020
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 commentedon Apr 23, 2021
Related to #386