search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
131 stars 33 forks source link

Windows support through Opam 2.2 #1150

Open AllanBlanchard opened 3 months ago

AllanBlanchard commented 3 months ago

FYI, we worked a little bit on porting Frama-C to Windows in Opam 2.2. We had to fix zlib and gmp which are also necessary for Alt-Ergo but we could not really figure out how to fix Alt-Ergo.

The fixes that we prepared are available here: https://github.com/ocaml/opam-repository/compare/master...zilbuz:opam-repository:frama-c-windows

In Alt-Ergo, I slightly modified /src/bin/text/dune, adding a condition enabled_if for the flags, and for now just adding a rule for Windows that uses the standard flags, however, if I can build the executable, it just fails to run currently, so I guess that diving in the code of Alt-Ergo might be necessary.

bclement-ocp commented 2 months ago

Thanks for the report & extra information. For tracking purposes: assigning @Halbaroth since this is essentially a duplicate of #919

Halbaroth commented 1 month ago

Good news, Alt-Ergo works on Windows through Opam 2.2 now! We support installations with both MSYS2 and Cygwin. You can try to setup it with:

opam pin https://github.com/OCamlPro/alt-ergo.git#next

Please, let me know if you have an issue.

Your patches have been helpful but when I tried it, I need to patch camlzip too and it seems I did something wrong because Alt-Ergo crashed frequently, depending on the environment in which we loaded it. I believed it was a problem related with the linked libraries but after some of patches of Basile Desloges have been pushed on opam-repository, everything works fine.

Alt-Ergo will officially support Windows in the next release 2.6.0, which should be published in September.

Notice that some features are not available on Windows (see #1201). We plan to support timelimit and :reproduce-resource-limit in 2.7.0. Tell me if you need it in the next release.

AllanBlanchard commented 4 weeks ago

Sorry for this long silence, I was in vacation ^^.

I installed the package this morning and got the following warning:

[WARNING] C:\Users\ab238114\AppData\Local\opam\default\bin\alt-ergo.exe is a Cygwin-linked executable

And when I try to run the exectuable, nothing happens but the return value is false:

PS C:\> alt-ergo.exe --version
PS C:\> echo $?
False

Notice that some features are not available on Windows (see https://github.com/OCamlPro/alt-ergo/issues/1201). We plan to support timelimit and :reproduce-resource-limit in 2.7.0. Tell me if you need it in the next release.

I guess that it means that Why3 will not be able to stop alt-ergo, but since Why3 still cannot compilable on Windows via Opam 2.2, I guess that it is not that problematic for us :P . From a business perspective it is not a problem for now: we have workaround for the very few people working on Windows and most of them do not use WP (thus, they do not use Alt-Ergo). It might be a "problem" for me for teaching in march 2025 if:

Halbaroth commented 4 weeks ago

Sorry for this long silence, I was in vacation ^^.

I installed the package this morning and got the following warning:

[WARNING] C:\Users\ab238114\AppData\Local\opam\default\bin\alt-ergo.exe is a Cygwin-linked executable

And when I try to run the exectuable, nothing happens but the return value is false:

PS C:\> alt-ergo.exe --version
PS C:\> echo $?
False

Notice that some features are not available on Windows (see #1201). We plan to support timelimit and :reproduce-resource-limit in 2.7.0. Tell me if you need it in the next release.

Thanks for the bug report. I will investigate. I need bit of information:

  1. Did you try to install Alt-Ergo with a fresh opam setup?
  2. Did you install Cygwin by yourself and you use the opam init script to setup Cygwin?
  3. Did you try to run Alt-Ergo in bash through Cygwin?

I guess that it means that Why3 will not be able to stop alt-ergo, but since Why3 still cannot compilable on Windows via Opam 2.2, I guess that it is not that problematic for us :P .

I didn't check but I guess that Why3 can kill a subprocess if it exceed the time limit. We plan to support timelimit on Windows through GC alarms.

From a business perspective it is not a problem for now: we have workaround for the very few people working on Windows and most of them do not use WP (thus, they do not use Alt-Ergo). It might be a "problem" for me for teaching in march 2025 if:

* we succeed in creating a Windows package for Frama-C before that,

* why3 works on Windows at this point,

* Alt-Ergo 2.7.0 is not released at this point.

We can publish a small release if you really need this feature before the 2.7.0.

AllanBlanchard commented 3 weeks ago

On this morning, I started from a clean opam. I do not have an existing Cygwin installation. Here is what I did:

And I get:

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of alt-ergo.dev failed at "dune build -p alt-ergo -j 3 --promote-install-files=false @install".

#=== ERROR while compiling alt-ergo.dev =======================================#
# context     2.2.1 | win32/x86_64 | ocaml.5.2.0 | pinned(git+https://github.com/OCamlPro/alt-ergo.git#next#d99264b13d320689e3b81e2934826dfa6cdb5632)
# path        ~\AppData\Local\opam\default\.opam-switch\build\alt-ergo.dev
# command     ~\AppData\Local\opam\default\bin\dune.exe build -p alt-ergo -j 3 --promote-install-files=false @install
# exit-code   1
# env-file    ~\AppData\Local\opam\log\alt-ergo-10528-5389f6.env
# output-file ~\AppData\Local\opam\log\alt-ergo-10528-5389f6.out
### output ###
# File "src/bin/text/dune", lines 23-25, characters 0-94:
# 23 | (rule
# 24 |   (target alt-ergo.1)
# 25 |   (action (with-stdout-to %{target} (run alt-ergo --help=groff))))
# (cd _build/default/src/bin/text && ./Main_text.exe --help=groff) > _build/default/src/bin/text/alt-ergo.1
# Command exited with code -1073741515.
Halbaroth commented 2 weeks ago

I tried again yesterday with a fresh installation of opam and I couldn't reproduce the bug. Could you try to run Alt-Ergo in bash with a dummy input? We may got an error.

While working on the Windows support, I got a similar issue. Sometimes Alt-Ergo failed with a very large negative return code. After some investigations, I discovered that the issue was related with linked libraries. I didn't find the origin of the issue (because I didn't manage to compile Cygwin with appropriate debug flag to catch the error) but the bug disappeared after upgrading opam packages. I guess the bug disappered by sheer luck.

We may have more information if you try to build Alt-Ergo from the source. Could you run these commands in bash?

git clone --depth 1 https://github.com/OCamlPro/alt-ergo.git
cd alt-ergo
make dev-switch
eval $(opam env)
make bin
make runtest
AllanBlanchard commented 2 weeks ago

Could you try to run Alt-Ergo in bash with a dummy input? We may got an error.

Currently the problem is that it does not build at all, so I can't run it.

We may have more information if you try to build Alt-Ergo from the source. Could you run these commands in bash?

Do you know if there is a way to do it in the Cygwin environment generated by Opam? Else, I will have to create a new one, and I am not sure it will be configured the same way.

Halbaroth commented 2 weeks ago

Actually Alt-Ergo built but we use the command alt-ergo --help=groff in a dune script to generate the man page after compiling the binary. The command failed and the installation aborted.

Sure, you can run bash for the Cygwin environment by lauching the binary bash.exe located in C:\Users\your_username\AppData\Local\opam\.cygwin\root\bin\bash.exe. On my setup, the PATH variable is not set correctly so I have to type:

export PATH=/cygdrive/c/Users/your_username/AppData/Local/opam/.cygwin/root/bin:$PATH

I believe that there is also an icon on your desktop to launch a bash terminal. In my case, I got a correct PATH in this way but I prefer using Windows through an ssh session.

AllanBlanchard commented 2 weeks ago

Running the build through bash allows to get a working executable. I tried to run the very same dune command directly in cmd and powershell with the opam environment setup and here is the kind of messages that I get:

0 [main] x86_64-w64-mingw32-gcc (27200) C:\Users\ab238114\AppData\Local\opam\.cygwin\root\bin\x86_64-w64-mingw32-gcc.exe: *** fatal error - add_item ("\??\C:\Users\ab238114\AppData\Local\opam\.cygwin\root", "/", ...) failed, errno 1
File "src/bin/text/dune", lines 13-20, characters 0-209:
13 | (executable
14 |   (name Main_text)
15 |   (public_name alt-ergo)
16 |   (package alt-ergo)
17 |   (libraries alt_ergo_common)
18 |   (link_flags (:standard (:include link_flags.dune)))
19 |   (modules Main_text)
20 |   (promote (until-clean)))
0 [main] x86_64-w64-mingw32-gcc (27200) C:\Users\ab238114\AppData\Local\opam\.cygwin\root\bin\x86_64-w64-mingw32-gcc.exe: *** fatal error - add_item ("\??\C:\Users\ab238114\AppData\Local\opam\.cygwin\root", "/", ...) failed, errno 1
File "src/bin/text/.Main_text.eobjs/dune_site_plugins__Dune_site_plugins_data.ml-gen", line 1
Error: Assembler error, input left in file C:\Users\ab238114\AppData\Local\Temp\build_f65dbe_dune\camlasm3cec8c.s

It seems that there is something in the build that is closely related to the environment.

Halbaroth commented 2 weeks ago

At least we have a message :) I tried to compile Alt-Ergo in cmd.exe with make bin and it works fine in my environment. Just to be sure we have the same Unix environment at least, could you send me the outputs of these commands:

Let's try to build it in cmd.exe with a minimal dune file. Replace all the content of src/bin/text/dune by

(executable
  (name Main_text)
  (public_name alt-ergo)
  (package alt-ergo)
  (libraries alt_ergo_common)
  (modules Main_text))

and run make bin in cmd.exe. Do you get an executable? Does it work?

EDIT: could send me the content of the file C:\Users\ab238114\AppData\Local\Temp\build_f65dbe_dune\camlasm3cec8c.s?

EDIT 2: we may run dune build with the flag --verbose in order to output the wrong command.

Halbaroth commented 2 weeks ago

It seems that the last error is output by the ocaml compiler and could come from a mismatch between the assembler of mingw and the generated assembler by the ocaml compiler. What is the output of ocamlopt -config and as --version?