Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Windows support through Opam 2.2 #1150

Open
AllanBlanchard opened this issue Jun 18, 2024 · 11 comments
Open

Windows support through Opam 2.2 #1150

AllanBlanchard opened this issue Jun 18, 2024 · 11 comments
Assignees
Labels
windows Relates to Windows support
Milestone

Comments

@AllanBlanchard
Copy link

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: ocaml/opam-repository@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 bclement-ocp added the triage Requires a decision from the dev team label Jul 11, 2024
@bclement-ocp bclement-ocp added this to the 2.6.0 milestone Jul 11, 2024
@bclement-ocp bclement-ocp removed the triage Requires a decision from the dev team label Jul 11, 2024
@bclement-ocp
Copy link
Collaborator

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

@Halbaroth
Copy link
Collaborator

Halbaroth commented Aug 9, 2024

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.

@Halbaroth Halbaroth added the windows Relates to Windows support label Aug 9, 2024
@AllanBlanchard
Copy link
Author

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.

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:

  • 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.

@Halbaroth
Copy link
Collaborator

Halbaroth commented Sep 6, 2024

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
Copy link
Author

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

  • installing Opam
  • opam init with internal Cygwin,
  • opam pin https://github.com/OCamlPro/alt-ergo.git#next

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
Copy link
Collaborator

Halbaroth commented Sep 17, 2024

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
Copy link
Author

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
Copy link
Collaborator

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
Copy link
Author

AllanBlanchard commented Sep 19, 2024

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
Copy link
Collaborator

Halbaroth commented Sep 19, 2024

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:

  • cygcheck.exe -V
  • opam --version
  • opam list

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
Copy link
Collaborator

Halbaroth commented Sep 19, 2024

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?

@bclement-ocp bclement-ocp modified the milestones: 2.6.0, 2.7.0 Oct 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
windows Relates to Windows support
Projects
None yet
Development

No branches or pull requests

3 participants