Skip to content

Fix build with dune package management #1319

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

Open
wants to merge 1 commit into
base: next
Choose a base branch
from

Conversation

Sudha247
Copy link

This PR adds some dependencies that fix building with dune package management. Happy to submit a PR to opam-repository retroactively changing it for released versions if it's appropriate.

@bclement-ocp
Copy link
Collaborator

Hi and thanks for the PR!

Can you clarify what commands you are using that are failing? These dependencies should only be required for building the JS version of alt-ergo, which is not intended to be built through opam.

@Sudha247
Copy link
Author

Thanks for the response! So my usual workflow is this --

$ dune pkg lock # To determine dependencies
$ dune build # Install dependencies and build the project

Doing this on the main branch results in the following error message:

File "src/lib/dune", line 44, characters 4-10:
44 |     Config Emap Gc_debug Hconsing Hstring Iheap Lists Loc
         ^^^^^^
Error: Module Config doesn't exist.
Error: Multiple rules generated for               
_build/default/src/bin/text/Main_text.exe:
- src/bin/text/dune:7
- file present in source tree
-> required by alias default
Hint: rm -f src/bin/text/Main_text.exe
File "src/bin/js/dune", line 4, characters 32-47:  
4 |   (libraries    alt_ergo_common zarith_stubs_js)
                                    ^^^^^^^^^^^^^^^
Error: Library "zarith_stubs_js" not found.
-> required by _build/default/src/bin/js/main_text_js.bc
-> required by alias src/bin/js/all
-> required by alias default
File "src/bin/js/dune", line 32, characters 61-76: 
32 |   (libraries    worker_interface zarith_stubs_js js_of_ocaml js_of_ocaml-lwt)
                                                                  ^^^^^^^^^^^^^^^
Error: Library "js_of_ocaml-lwt" not found.
-> required by _build/default/src/bin/js/worker_example.bc
-> required by alias src/bin/js/all
-> required by alias default
File "src/bin/js/dune", line 21, characters 77-92: 
21 |   (libraries    worker_interface alt_ergo_common zarith_stubs_js js_of_ocaml js_of_ocaml-lwt)
                                                                                  ^^^^^^^^^^^^^^^
Error: Library "js_of_ocaml-lwt" not found.
-> required by _build/default/src/bin/js/worker_js.bc
-> required by alias src/bin/js/all
-> required by alias default
File "src/bin/js/dune", line 14, characters 28-41: 
14 |   (libraries    js_of_ocaml data-encoding)
                                 ^^^^^^^^^^^^^
Error: Library "data-encoding" not found.
-> required by library "worker_interface" in _build/default/src/bin/js
-> required by
   _build/default/src/bin/js/.worker_interface.objs/native/worker_interface.cmx
-> required by _build/default/src/bin/js/worker_interface.a
-> required by alias src/bin/js/all
-> required by alias default
Error: Program js_of_ocaml not found in the tree or in PATH
 (context: default)
-> required by _build/default/src/bin/js/main_text_js.bc.js
-> required by alias src/bin/js/all
-> required by alias default
Hint: opam install js_of_ocaml-compiler
File "src/bin/js/dune", line 35, characters 19-34: 
35 |   (preprocess (pps js_of_ocaml-ppx lwt_ppx))
                        ^^^^^^^^^^^^^^^
Error: Library "js_of_ocaml-ppx" not found.
-> required by _build/default/src/bin/js/worker_example.pp.ml
-> required by alias src/bin/js/all
-> required by alias default
File "src/plugins/AB-Why3/dune", lines 8-12, characters 0-84:
 8 | (menhir
 9 |   (infer    false)
10 |   (flags    --fixed-exception)
11 |   (modules  why3_parser)
12 | )
Error: the code back-end requires the type of every nonterminal symbol to be
known. Please specify the type of every symbol via %type declarations, or
enable type inference (look up --infer in the manual).
Type inference is automatically enabled when Menhir is used via Dune,
provided the dune-project file says (using menhir 2.0) or later.

I suspect this is because dune build tries to build the whole repo.

@bclement-ocp
Copy link
Collaborator

Doing this on the main branch results in the following error message:

You should be using the next branch (which is the default branch for the repository), not the main branch which is an old branch (the naming is confusing, I know…).

@bclement-ocp
Copy link
Collaborator

That said, you are right that dune build will try to build everything (including js stuff), as does make (I usually only do either dune exec -- alt-ergo or dune build @runtest).

We can't really add those as dependencies, because they are not used unless buildin with JS, and it's not really appropriate to add them as with-dev dependencies either (for the same reason). Ideally, we should have a separate alt-ergo-js package to attach these dependencies to, but I think we had problems with this in the past (although I don't recall exactly what).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants