Stream: Coq users

Topic: CompCert on Windows


view this post on Zulip Andre (Dec 07 2023 at 14:49):

Hello,

I'm trying to install Coq on Windows (via Cygwin), so that I can then compile a custom version of CompCert, and use it to compile Windows-native programs. There's one restriction: I can't use WSL (company policy disables virtualization).

First, I tried simply installing Cygwin, then opam, then opam install coq, but it failed with an error related to dllzarith.so. Some googling indicated that this was a known issue, and the solution was to install Coq using Coq platform.

Then I tried using Coq platform, and managed to install it, both using the Windows installer, and by compiling sources using opam on Cygwin, but in both cases, I have some issues:

Given that CompCert is installable from Coq platform, I assume someone got it working, so I wonder if I am doing something obviously wrong. Are there any reports of people who are actually using CompCert (3.12 or 3.13) from Windows, to compile Windows binaries?

view this post on Zulip Michael Soegtrop (Dec 07 2023 at 15:07):

@Andre :

In the Windows installer gcc is not includes. CompCert is mostly included to support the VST based lectures, which concentrate on verifying code. But it does work if you install a MinGW gcc by other means and put it into the path.

When you use the script variant you need to be very careful which gcc variant you use. The default gcc is a cygwin gcc, but CompCert is MinGW, so you must make sure that the mingw gcc is in PATH before the cygwin gcc. Both variants of gcc are included in the cygwin installation. The resulting executables should be MinGW executables and not depend on cygwin.dll.

The cygwin build is technically a cross compilation with cygwin as build host and MinGW as target - it is similar to compiling Windows apps on Linux. This complicates the situation quite a bit.

I guess I should add a script to prepare the environment for compcert compilation.

view this post on Zulip Andre (Dec 07 2023 at 15:21):

Thank you for the clarification. I did see MinGW mentioned inthe installer, but I didn't check to see that it was installed. I'll try adding it to the PATH in front of the other, and see what happens.

view this post on Zulip Michael Soegtrop (Dec 07 2023 at 15:28):

I am not currently at a Windows machine - if you need help finding the MinGW gcc in the cygwin directory structure, please let me know.

view this post on Zulip Andre (Dec 07 2023 at 16:31):

Actually, it seems that simply adding a -toolprefix x86_64-w64-mingw32- option to CompCert allowed it to find the MinGW compiler instead of the Cygwin one.

Now I'm having another issue, but possibly completely unrelated to CompCert and Coq:

In the file included from /usr/x86_64-w64-mingw32/sys-root/mingw/include/_mingw.h:282,
                 from /usr/x86_64-w64-mingw32/sys-root/mingw/include/corecrt.h:10,
                 from /usr/x86_64-w64-mingw32/sys-root/mingw/include/corecrt_stdio_config.h:10,
                 from /usr/x86_64-w64-mingw32/sys-root/mingw/include/stdio.h:9,
                 from a.c:1:
/usr/x86_64-w64-mingw32/sys-root/mingw/include/vadefs.h:35:2: error: #error VARARGS not implemented for this compiler

I'll try another version of CompCert to see if that helps, but in any case I think the "Coq platform" part is not the issue here...

view this post on Zulip Michael Soegtrop (Dec 07 2023 at 17:26):

I am not so sure how this works with CompCert, but it comes with its own header files, and I think it should be using these.

Did you have a look at CompCert Manual

view this post on Zulip Andre (Dec 07 2023 at 18:30):

I just tried to compile:

#include <stdio.h>
int main() {
  printf("hello world\n");
  return 0;
}

If I remove the #include <stdio.h> (and the call to printf) it works (I can compile a simple program that returns a non-zero value), but stdio.h is kind of useful...

The CompCert manual just mentions Windows and Cygwin without many details. It does not mention MinGW, for instance. For now, however, the MinGW version actually works better than my previous attempt with Cygwin (which compiled, but did nothing when executed).

view this post on Zulip Michael Soegtrop (Dec 08 2023 at 08:50):

@Andre: I see these include files in my installation (MacOS):

./lib/compcert/include/stdalign.h
./lib/compcert/include/stdnoreturn.h
./lib/compcert/include/float.h
./lib/compcert/include/stddef.h
./lib/compcert/include/stdbool.h
./lib/compcert/include/varargs.h
./lib/compcert/include/stdarg.h

I guess you have the same. Please have a look at:

https://github.com/AbsInt/CompCert/blob/master/runtime/include/varargs.h

so CompCert does not implement old style varargs, but it does implement the newer (standard since the 90s or so) stadarg.h. Why the MinGW stdio.h requires vararg.h I can't tell - it might be an odd configuration choice. If this is specific to the cygwin MinGW distribution I don't know - it is possible.

Btw.: CompCert does not come with a formally verified version of printf - you can call from CompCert into external libraries, but you leave a formally verified path then. When you need to write formally verified code which uses printf, I guess you have to write a formally verified variant of printf with CompCert - at which point the problems go away. Princeton is working on standard library C functions for CompCert, but no printf as yet. See https://www.cs.princeton.edu/~appel/papers/vstlib.pdf.

Going a little step in this direction would be to compile the GNU C library with CompCert (rather than with MinGW gcc). The vararg issue should go away then, because the configure script would figure out that it is not supported. Not sure if this has been done / is common practice.

It is time to ask @Xavier Leroy for help.


Last updated: Jun 13 2024 at 21:01 UTC