[ci] GH actions for windows, linux and osx

[gares]

I've extracted from #44 the commit adding CI to the platform, based on work by @Zimmi48. Two things before merge:

• avoid the GH action to run CI twice (see this PR, it's both a push and a pull_request)
• fix the windows job (I kind of recall having seen the bad file descriptor problem before)

This commit should work just fine on the v8.12 branch

[Zimmi48]

I don't deserve to be the only "author" of this commit.

[gares]

I don't deserve to be the only "author" of this commit.

tell git, I did nothing special ;-)

[Zimmi48]

I don't deserve to be the only "author" of this commit.

tell git, I did nothing special ;-)

What I meant is that you can --reset-author on this commit. If you want, you can add me as co-author.

[Zimmi48]

BTW, you may also want to add scheduled pipelines. See rocq-community/templates#77 for hints on how to do so.

[gares]

Yes! I plan to do that for the other PR, the one using Coq's overlays

[gares]

I'm stuck here (on windows):

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed opam-depext.1.1.5
Done.
# Run eval $(opam env) to update the current shell environment

<><> Carrying on to "C:\cygwin64_coq_platform\usr\x86_64-w64-mingw32\sys-root\mingw\bin\opam.exe depext conf-gtksourceview3" 

# Detecting depexts using vars: arch=x86_64, os=win32, os-distribution=cygwinports, os-family=windows
# The following system packages are needed:
Fatal error: exception Sys_error("Bad file descriptor")
ERROR coq_platform_make_windows.bat failed

@MSoegtropIMC if this rings a bell, I'm all ears. (I think we saw that already, but I can't remember what the problem was)

[MSoegtropIMC]

This might be connected to #45: Please make sure that any paths you give on the command line of the batch file have double back slashes or forward slashes might also work. Or alternatively I can fix #45, but it might take an hour or two.

[gares]

Thanks, I'll try that!

[gares]

@MSoegtropIMC I tried a workaround, see last commit, but does not seem to cut it. I'll try to reproduce it locally after lunch (the only difference I see is that here I don't use an administrative cygwin...)

[MSoegtropIMC]

I frequently also test to download the zip and run the batch file from a dos console. This did work. Can you check if the paths in the parameter overview dump look correct?

[gares]

They look ok, with double \ (but for the cache, which I did not pass explicitly)

Parameter values (default or currently set):
(Run "coq_platform_make_windows -h" for details)
-arch     = x86_64
-build    = y
-destcyg  = C:\\cygwin64_coq_platform
-proxy    =  
-cygrepo  = https://mirrors.kernel.org/sourceware/cygwin
-cygcache = C:\Users\RUNNER~1\AppData\Local\Temp\coq_platform_cygwin_cache
-cyglocal = n
-cygquiet = y
-cygforce = n
-extent   = f
-parallel = p
-jobs     = 2
-compcert = f
-vst      = y
-switch   = 
CYGWIN INSTALL DIR (WIN)    = C:\\cygwin64_coq_platform
CYGWIN INSTALL DIR (MINGW)  = C://cygwin64_coq_platform
CYGWIN INSTALL DIR (CYGWIN) = /cygdrive/c//cygwin64_coq_platform

[gares]

I cannot reproduce it locally, so I'm sneaking in --verbose and see how it goes.

[MSoegtropIMC]

One more thought: I think I might have one more bug: the ARCH variable is I think redefined in an inconsistent way somewhere (from / to 32/64 to i686/x86_64) and having ARCH defined before you start the batch file can lead to unwanted effects.

[MSoegtropIMC]

@gares : please ping me when a build is finished before you change something, so that I can inspect the logs.

[gares]

Old logs are available, click on the red x next to the commit hash in this discussion, or even better on the actions tab next to pull requests.

[gares]

It failed again, we now have a little backtrace from ocaml

# Detecting depexts using vars: arch=x86_64, os=win32, os-distribution=cygwinports, os-family=windows
# The following system packages are needed:
Fatal error: exception Sys_error("Bad file descriptor")
Raised by primitive operation at file "camlinternalFormat.ml", line 1876, characters 48-55
Called from file "printf.ml", line 20, characters 28-44
Called from file "depext.ml", line 442, characters 6-61
Called from file "cmdliner/src/cmdliner.ml", line 1350, characters 17-26
Called from file "cmdliner/src/cmdliner.ml", line 1375, characters 8-50
Called from file "depext.ml", line 602, characters 10-40
ERROR coq_platform_make_windows.bat failed

[MSoegtropIMC]

@gares : I think it is going wild long before. E.g. in the script before === OPAM REPOSITORIES === it does an eval $(opam env) , so after this one should never see # Run eval $(opam env) to update the current shell environment, but one does. Also it is weird that it tries to install depext after installing depext-cygwin - I need to compare the logs with a local build.

Maybe it ends up in a bad switch by some magic. I would insert some opam switch and opam list commands after each step of the opam initialization (install-opam.sh). Maybe some carriage return in the switch name or so.

[gares]

From
https://github.com/ocaml/ocaml/blob/4135828a4b66eb7403d68839da701257c0ccd31e/stdlib/camlinternalFormat.ml#L1876
is seems a call to flush.
File depext.ml from tag 1.1.5 from https://github.com/ocaml-opam/opam-depext/releases ha no line 602...so I can't say what line 442 does either... From the logs it seems we use 1.1.5, so I'm a bit puzzled. Are we using a "custom fork" on windows?

[MSoegtropIMC]

@gares: I think there is one depext.ml from depext-cygwin and one from depext plain.

[MSoegtropIMC]

Btw.: in order to get this working for now you can simply disable depext on cygwin - it should not be required, I add all packages to the cygwin setup. I just added it for adding depext for additional opam packages by the user later.

But I would really like to track this down - looks like something which could happen to users as well.

Also: can you add a SET command in the batch file at a few points and maybe an env command in the shell script here and there?

[gares]

I see, the hypothesis is that -> installed depext-cygwinports.0.0.7 did not really install depext, so it tries to install and use the non cygwin one and it blows up.
I added some prints, I can add more, but I think we have a lead.

[MSoegtropIMC]

I see, the hypothesis is that -> installed depext-cygwinports.0.0.7 did not really install depext, so it tries to install and use the non cygwin one and it blows up.

I am not 100% sure if this not normal. I want to compare the logs with a local build, but I am in meetings until one hour from now.

[gares]

OK, no problem. Also feel free to push on this branch any commit you like adding prints. I'm going to play with my solder tonight, not with CI ;-)

[MSoegtropIMC]

@gares : I compared it with the log from a local build and it is pretty much identical up the point it dies. Need to sleep over this ...

[MSoegtropIMC]

@gares : I have a few ideas what this might be - let me do a few tests. I will ping you when I am through with my ideas.

[MSoegtropIMC]

@gares : one question: why do you install opam manually on Ubuntu and MacOS? The script should do thsi automatically. Maybe on MacOS this can be improved (it does it via Homebrew or MacPorts and fails if neither is there) but on Ubuntu this does work.

[gares]

You suggested to do so (do u recall I wanted to add REGTEST on unix since the opam installer asks questions).

[gares]

%USER%

OK, I'll give it a try. The doc is not super clear about wildcards and windows paths: https://docs.github.com/en/free-pro-team@latest/actions/guides/storing-workflow-data-as-artifacts

BTW, it is possible to pass artifacts to other jobs (see the last example in the doc above). Maybe we can also try to run the installer by passing /D=C:\Coq as per
https://nsis.sourceforge.io/Docs/Chapter3.html , but I've no idea how to test if CoqIDE can start.

[MSoegtropIMC]

BTW, it is possible to pass artifacts to other jobs (see the last example in the doc above).

Sorry I don't know - I think you know more about CI than I do (and I am very grateful that you went through this effort!)

Maybe we can also try to run the installer

It should work with "installer /S /D=dir", but it needs to be run from an admin console to avoid the rights elevation question.

[MSoegtropIMC]

Quite bizarre this depext issue, btw. Not sure why it works in local builds if one is installed after the other. But then depext-cygwinports is version 0.0.7, so I guess there is nobody to blame. But I wonder if I should include it. As I said, I don't need it for anything which is in the platform - I install all packages upfront. This is mostly for the convenience of users who want to install additional packages.

[MSoegtropIMC]

@Zimmi48 : a few more notes on MSYS2 and Cygwin:

• Cygwin is officially supported by CompCert (since 3.8. for both 32 and 64 bit).
• Back then it was more effort to compile CoqIDE with MSYS2 than to compile CoqIDE, GTK and all prerequisites which did not exist in Cygwin back than (20 or so) from sources.
• Right now the gtksourceview package is outdated in cygwin - it has a severe bug. I need to compile a new one (it has no maintainer in Cygwin right now). I would expect that this is better in MSYS2.

[gares]

It should work with "installer /S /D=dir", but it needs to be run from an admin console to avoid the rights elevation question.

After miserably failing to find a way to start a cmd.exe in admin mode on the internet, the good news is that on GH actions:

Windows virtual machines are configured to run as administrators with User Account Control (UAC) disabled. For more information, see "How User Account Control works" in the Windows documentation.

[MSoegtropIMC]

the good news is that on GH actions

I should have told you that this is my guess. It is rather tricky to do anything unattended otherwise.

[gares]

The silly broken log feed spoke: -> installed coq-compcert.3.8. Hurray!

[MSoegtropIMC]

The silly broken log feed spoke: -> installed coq-compcert.3.8. Hurray!

I can't see the log yet, but I think we can conclude that the depext issue is solved, so I give this back to you.

I will take care of finishing the installer creator (it has a few bugs, stuff like style files are missing and the like). Half done.

[gares]

The log thing is buggy, now I see nothing, but a few minutes back it did spit that line, so I guess it's working (and crunching on vst)

I'm back on track, thanks!

[MSoegtropIMC]

The log thing is buggy, now I see nothing

I downloaded the zip with logs and I see the "FINISHED" line. It failed on the wrong installer creation command now.

I'm back on track, thanks!

I say thank you! Without your effort it would have taken another few months until we would have had CI for the Coq platform.

[MSoegtropIMC]

@gares : FYI: I am almost finished with a script to produce a set of smoke test files (one or two for each installed library / plugin) and batch and shell scripts to run them through coqc. This can be later used to extend your smoke test, so no need to work on that.

[gares]

OK. The last commit here separates the windows job into two parts, the first one build the installer, the second one downloads it and runs silly tests. The question is: do you need cygwin to run the tests? Because artifacts are max 2G (per repository if I get it right) so I can't put the entire cygwin inside the artifact. We can go back to 1 job (time limit is fine) or rebuild a fresh environment for smoke testing.

EDIT: I now see you say batch and shell so I guess you have a .bat which is perfect.

[MSoegtropIMC]

I need a shell and opam to create the smoke test kit, but it is very small and can be uploaded together with the installer or even be installed (would make sense). Running the smoke test kit just needs what has been installed.

[Blaisorblade]

Is dsiable a typo?

[gares]

eh eh, yes