Karl Palmskog (Aug 28 2020 at 21:37): Karl Palmskog (Aug 28 2020 at 21:37):After I installed coq-compcert-64 (non-open-source 3.7 version), I had no clightgen executable. However, for coq-compcert it turns up just fine. Is this a bug or intended?
Karl Palmskog (Aug 29 2020 at 12:45):I at least managed to do something I wanted to do for a few years now: set up a completely standalone Coq project with CI that verifies C code using VST (32-bit version for now): https://github.com/palmskog/vst-array-progs -- any other kind of verification of Java-like programs in Coq is seemingly dead (Why and Frama-C had a toolchain, but either obsolete or deprecated now)
Michael Soegtrop (Aug 29 2020 at 13:23):As documented in the opam package (which should be shown to the user), the 64 bit files are not installed in the usual folders and thus are usually not in the PATH. Can you please check the notes in https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-compcert-64/coq-compcert-64.3.7%7Ecoq-platform/opam and comment if it is as documented there?
Karl Palmskog (Aug 29 2020 at 13:27):I think the problem is that binaries not under bin are incredibly hard to use (in particular a big chore in CI). Why not rename them to ccomp64 and clightgen64 and in regular location?
Michael Soegtrop (Aug 29 2020 at 13:34):My assumption was that uses simply add this to the begin of PATH. Then make should pick this up automatically. This has the advantage that one can change the target platform just by changing PATH and keep everything else as is.
It might be tricky to work just with renamed compilers since one also needs (in general) different libraries, include files and so on. In my experience it is common to put non standard build environments into separate folders. In cygwin for MinGW cross, they have both - the bare name under special folders and modified names.
One could rename the files, but this would either require some hacking or changes in the CompCert make files. My plan is to avoid this unless there are really reasons why people can't live with this as is.
Please also note that it would make sense to install CompCert cross compilers, say for ARM Linux, so the name should probably by a fully qualified name then, not just ccomp64.
Michael Soegtrop (Aug 29 2020 at 13:34):P.S.: Likely with CompCert 3.8 the default will switch to 64 bit.
Karl Palmskog (Aug 29 2020 at 13:37):I don't think we have any support at the moment for setting the PATH in the GitHub Action CI, so for me at least binaries elsewhere is a showstopper. But if this will go away in 3.8 I guess it's alright.
Michael Soegtrop (Aug 29 2020 at 13:42):Hmm, not sure what the issue is here - isn't any CI job in the end a shell script where you can set PATh at will? Also if you use opam, things anyway end up under ~/.opam/<switch>/bin. If this can be added to PATH, it should be possible to add ~/.opam/<switch>/variant64/bin as well. I guess GitHub doesn't have special support for opam.
Karl Palmskog (Aug 29 2020 at 13:44):here is an example GitHub Actions Coq CI configuration: https://github.com/palmskog/vst-array-progs/blob/master/.github/workflows/coq-ci.yml
Basically, one will need to tell it somehow that PATH should be augmented with some path that depends on the current OPAM switch. There is no variable for this, and it will likely take some work to figure out how it should be best parameterized.
Karl Palmskog (Aug 29 2020 at 13:46):my plan was to set up Dune rules for clightgen to generate the Coq code, and have tests that use ccomp, etc. This can at least be done out-of-the-box with 32-bit 3.7, so I'll go with that for now.
Michael Soegtrop (Aug 29 2020 at 15:09):here is an example GitHub Actions Coq CI configuration: https://github.com/palmskog/vst-array-progs/blob/master/.github/workflows/coq-ci.yml
Basically, one will need to tell it somehow that
PATHshould be augmented with some path that depends on the current OPAM switch. There is no variable for this, and it will likely take some work to figure out how it should be best parameterized.
OK, this is a very specialized action using a specific docker image - I guess one could extend it accordingly.
Karl Palmskog (Aug 30 2020 at 13:57):building just CompCert and VST takes around 1 hour in the GitHub Actions CI. This is why I'm looking forward to the Docker images with the initial Coq platform - build time would probably be a few minutes for any VST-based project.
Karl Palmskog (Sep 02 2020 at 01:30):the following spec seems a bit much just to be guaranteed to get clightgen across both 8.11 and 8.12:
depends: [
"coq" {>= "8.11" & < "8.13~"}
"coq-compcert" {(= "3.7~coq_platform") | (= "3.7+8.12~coq_platform")}
"coq-vst" {>= "2.6" & < "2.7~"}
]
Well it's only the one line isn't it? I fear it doesn't get any easier. This is because Clightgen is not free software and one has to distinguish the free and the non free parts. One could have separate packages for the free part, clightgen and ccomp but this wouldn't be terribly efficient from a build time point of view.
I guess the best solution would be to have meta packages for the open source part, clightgen and ccomp and to make sure that the open source package is "newer".
But I am open to discussions - if you have a better idea, please let me know.
Karl Palmskog (Sep 02 2020 at 08:33):thanks, I think I understand the issues, but no obvious improvement comes to mind. I will continue the experiment with working with latest VST on both 8.11 and 8.12.
Michael Soegtrop (Sep 02 2020 at 08:49):How about the idea to create a meta package for the open source part (VST depends on), cligthgen and ccomp?
Karl Palmskog (Sep 02 2020 at 08:57):maybe, but I have a hard time seeing how the dependencies would go. Perhaps there should be separate coq-clightgen and coq-ccomp packages, since these have independent uses.
Karl Palmskog (Sep 02 2020 at 09:04):the whole license conundrum is pretty baffling, I guess I will have to read up on how the non-free parts of CompCert would affect my code. Whenever I have license problems, it's always due to one of (1) academic non-open-source licenses or (2) GPL. It looks like CompCert is one of the rare 2-in-1.
Karl Palmskog (Sep 02 2020 at 09:12):@Michael Soegtrop hmm I was looking through the CompCert license, and it looks like clightgen is actually dual-licensed under both the non-commercial license and GPL-2.0-or-later?
Karl Palmskog (Sep 02 2020 at 09:12):specifically, https://github.com/AbsInt/CompCert/blob/master/LICENSE#L47
given this, am I missing something why coq-compcert.3.7~coq-platform~open-source does not provide clightgen?
Michael Soegtrop (Sep 02 2020 at 10:27):Michael Soegtrop hmm I was looking through the CompCert license, and it looks like
clightgenis actually dual-licensed under both the non-commercial license and GPL-2.0-or-later?
Clightgen is definitely not free - I agree that one might assume that clightgen consists of exactly the files listed as open source, but it needs an additional stage of the compiler which is not free. I am 100% sure about this because I had extensive discussions on this with Xavier. Also you can buy a license for clightgen from AbsInt.
Michael Soegtrop (Sep 02 2020 at 10:30):maybe, but I have a hard time seeing how the dependencies would go. Perhaps there should be separate
coq-clightgenandcoq-ccomppackages, since these have independent uses.
Yes, this is what I meant, but made such that they depend on coq-compcert~coq-platform. One could also make experiments to build them separately and see how long this takes compared to building them together.
Michael Soegtrop (Sep 02 2020 at 10:31):Is the thumb up for "depends on coq-compcert~coq-platform" or "make experiments ..." ?
Karl Palmskog (Sep 02 2020 at 10:33):Michael Soegtrop said:
Clightgen is definitely not free - I agree that one might assume that clightgen consists of exactly the files listed as open source, but it needs an additional stage of the compiler which is not free. I am 100% sure about this because I had extensive discussions on this with Xavier. Also you can buy a license for clightgen from AbsInt.
OK I see. Given that I work in research, I think I am covered by the educational license for the moment. I guess licenses will be time-limited as well, so I don't think there's any way for me to make it economical to go outside the educational license.
Karl Palmskog (Sep 02 2020 at 10:34):Michael Soegtrop said:
Is the thumb up for "depends on coq-compcert~coq-platform" or "make experiments ..." ?
Regardless of whether clightgen and ccomp save time to build separately, I think packaging them separately and depending on coq-compcert~coq_platform could be worth trying out. At least it would make subprojects using VST much more convenient. I'm not sure how much effort this is "worth" at the moment though. VST probably has very few users.
Karl Palmskog (Sep 02 2020 at 10:48):one lesson I take from the "clightgen conundrum" is at least to not force consumers of my VST-based projects to call clightgen, but to have clightgen-generated code in version control (like they have in VST)
Michael Soegtrop (Sep 02 2020 at 12:32):one lesson I take from the "clightgen conundrum" is at least to not force consumers of my VST-based projects to call
clightgen, but to have clightgen-generated code in version control (like they have in VST)
yes, this is a good idea if you want industry people to try it. Even if the CompCert license allows evaluation, for industry any non standard license usually means to consult the law team.
Karl Palmskog (Sep 02 2020 at 12:39):Michael Soegtrop said:
yes, this is a good idea if you want industry people to try it. Even if the CompCert license allows evaluation, for industry any non standard license usually means to consult the law team.
Done now (and also meant coq-vst >= "3.7~" suffices). I have to confess I have almost given up on any evangelizing on low-level program verification for general industry, when the attitude is so much more positive among blockchain companies/organizations even on high-level protocol verification.
Last updated: Jun 03 2023 at 03:01 UTC