Benedikt Ahrens (Apr 26 2022 at 09:22): Benedikt Ahrens (Apr 26 2022 at 09:22):I am fascinated by the possibility of using Coq in the browser, in particular, for education - thanks for building jsCoq.
Is there a way to build and host one's own instance of jsCoq, with more libraries (I am particularly interested in UniMath) and custom commandline options (such as -noinit)? I would be very grateful for any pointers.
Ali Caglayan (Apr 26 2022 at 09:47):Hi Benedikt. AFAIK the answer to your questions are yes. We have built and hosted the HoTT library using jscoq in the past (so that means -noinit). The examples from the README.md for jscoq contains various project setups: https://github.com/jscoq/jscoq#examples
Ali Caglayan (Apr 26 2022 at 09:47):Here is the HoTT library for example: https://x80.org/rhino-hott/
Ali Caglayan (Apr 26 2022 at 09:48):I am not sure of the details of setting these up however so you will have to wait for more knowledgeable people to chime in.
Ali Caglayan (Apr 26 2022 at 09:49):cc @Emilio Jesús Gallego Arias
Hanneli Tavante (Apr 26 2022 at 14:30):"build and host one's own instance of jsCoq" <- I've been doing it with a Docker image https://github.com/jscoq/jscoq/blob/v8.14/etc/docker/Dockerfile
Emilio Jesús Gallego Arias (Apr 26 2022 at 16:54):Using docker is your best bet for now. We need to improve the build setup a bit better tho, if you have cycles to help we'd be very happy to help. There is an upcoming dune hackathon that should solve the most pressing issue of building soundly multiple theories.
The way I see the jsCoq distro tho is inspired by the system Shachar implemented w.r.t. lazy loading. It should be possible just to have jsCoq load lazily a lot of libs. One little problem tho is how to handle versioning, we don't have anything in the build system to support multiple versions.
Emilio Jesús Gallego Arias (Apr 26 2022 at 16:56):@Benedikt Ahrens note that these days HoTT doesn't require a special build anymore, so with a bit of work we should be able to have it standard in the jsCoq distribution.
Benedikt Ahrens (Apr 26 2022 at 17:34):Emilio Jesús Gallego Arias said:
Benedikt Ahrens note that these days HoTT doesn't require a special build anymore, so with a bit of work we should be able to have it standard in the jsCoq distribution.
That would be fantastic. Note that I am interested in UniMath, not in HoTT. However, the situation is similar; in particular, both are part of the Coq Platform.
Emilio Jesús Gallego Arias (Apr 26 2022 at 17:40):Great @Benedikt Ahrens ; I think packaging unimath should be simple, main problem may be the documentation of how to do it.
So I suggest we try together and fixup the jscoq docs on the way.
Benedikt Ahrens (Apr 27 2022 at 11:25):@Emilio Jesús Gallego Arias Yes, that would be great. I don't have any knowledge how to use docker, but I am happy to spend time on learning it.
Emilio Jesús Gallego Arias (Apr 27 2022 at 11:29):@Benedikt Ahrens docker knowledge should not really required, we use docker to build as a way to provide a common VM for all users, but the build script is just a few calls to the makefiles. Coq doesn't have an ABI so Docker provides a reproducible enviroment for everyone.
Emilio Jesús Gallego Arias (Apr 27 2022 at 11:29):I guess I would just start from some of the addons in https://github.com/jscoq/ and do unitmath that way
Benedikt Ahrens (Apr 27 2022 at 16:39):Thanks, I'll take a look!
Arnoud van der Leer (Mar 30 2023 at 22:12):Hi. I am puzzling to get this working. Currently, I get it to compile most of the code, but I get some errors:
# Use current workspace, not jsCoq's
npx jscoq sdk dune build
coqc UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesReordered.{glob,vo} (exit 1)
File "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesReordered.v", line 19, characters 32-34:
Error:
In environment
C : category
tu : tensor_unit C
The term "tu" has type "tensor_unit C" while it is expected to have type
"tensor_data ?C".
coqc UniMath/CategoryTheory/Monoidal/Examples/CartesianMonoidal.{glob,vo} (exit 1)
File "./UniMath/CategoryTheory/Monoidal/Examples/CartesianMonoidal.v", line 103, characters 12-29:
Error:
In environment
C : category
CP : BinProducts C
terminal : Terminal C
The term "tensorfrombinprod" has type "bifunctor C C C"
while it is expected to have type "tensor_data C".
coqc UniMath/CategoryTheory/Monoidal/Examples/EndofunctorsMonoidalElementary.{glob,vo} (exit 1)
File "./UniMath/CategoryTheory/Monoidal/Examples/EndofunctorsMonoidalElementary.v", line 51, characters 12-29:
Error:
In environment
C : category
The term "monendocat_tensor" has type "bifunctor [C, C] [C, C] [C, C]"
while it is expected to have type "tensor_data [C, C]".
coqc UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.{glob,vo} (exit 1)
File "./UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v", line 73, characters 2-40:
Warning: DAG_to_cat does not respect the uniform inheritance condition
[uniform-inheritance,typechecker]
File "./UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v", line 75, characters 46-47:
Error:
In environment
C : DAG
The term "C" has type "ob DAG" while it is expected to have type "category".
coqc UniMath/Bicategories/MonoidalCategories/EquivalenceActegoriesAndActions.{glob,vo} (exit 1)
File "./UniMath/Bicategories/MonoidalCategories/EquivalenceActegoriesAndActions.v", line 167, characters 33-82:
Error:
In environment
V : category
Mon_V : monoidal V
ax2 : actionbicat_ax2 Mon_V bicat_of_cats
C : bicatactionbicat Mon_V bicat_of_cats ax2
The term "bifunctor_from_functorintoendofunctorcat action_C" has type
"bifunctor V (pr1 C) (pr1 C)" while it is expected to have type
"action_data ?C".
npm ERR! code 1
npm ERR! path /media/arnoud/Common/work/uni_j8/side-job/jscoq
npm ERR! command failed
npm ERR! command sh -c jscoq "sdk" "dune" "build"
npm ERR! A complete log of this run can be found in:
npm ERR! /home/arnoud/.npm/_logs/2023-03-30T22_07_58_425Z-debug.log
make: *** [Makefile:9: build] Error 1
arnoud@elmo:/media/arnoud/Common/work/uni_j8/side-job/jscoq$
Someone suggested that it may have something to do with the version of coq (we get problems if it is below 8.15). Which version of coq/coqc is used to compile the addons? Is it 8.11, 8.15 or 8.16?
Arnoud van der Leer (Mar 30 2023 at 22:14):(So which version of coq handles the npx jscoq sdk dune build command?)
Emilio Jesús Gallego Arias (Mar 30 2023 at 23:19):Hi @Arnoud van der Leer , npx jscoq will likely pick Coq 8.16 as it is the latest available in npm
Emilio Jesús Gallego Arias (Mar 30 2023 at 23:20):Indeed the problem seems that the unimath version may not be compatible with 8.16?
Arnoud van der Leer (Mar 31 2023 at 07:34):Well, actually UniMath compiles fine on my machine with version 8.16
Arnoud van der Leer (Mar 31 2023 at 07:35):Is there a way to check or force which version of coq it is compiling against?
Emilio Jesús Gallego Arias (Mar 31 2023 at 14:15):Yes, using npm exec --package=<pkg>@version -- cmd should do the trick as to pick the right jscoq version
Emilio Jesús Gallego Arias (Mar 31 2023 at 14:15):Something to check is if the dune file in the unimath addons is up to date; the problem could be that jscoq is compiling more files than the ones specified in unimath
Emilio Jesús Gallego Arias (Mar 31 2023 at 14:32):Best way for us would be to check the addons build in the CI, I think we do but maybe not for all the interesting ones.
Arnoud van der Leer (Mar 31 2023 at 14:33):Well, it looks like I was indeed compiling using the old version of jscoq. However, now I get an error Error: File /opt/jscoq-sdk/coqlib/Coq/Init/Notations.vo has bad version number 81600 (expected 81500). It is corrupted or was compiled with another
version of Coq.. I am not entirely sure what the problem is there, but it looks like a mismatch between the compiler and the standard library that it uses?
Emilio Jesús Gallego Arias (Mar 31 2023 at 14:58):Yes, somehow you are calling Coq 8.15 with a 8.16 library
Emilio Jesús Gallego Arias (Mar 31 2023 at 14:59):Maybe you can try open an issue in the jsCoq repos outlining all the steps you've done from the start?
Arnoud van der Leer (Apr 14 2023 at 15:42):Hi. Thank you for the work you have been doing on this project. I have been doing other things, but now I have taken another look at JSCoq.
I have added my attempt to the following repository: https://github.com/UniMath/UniMath-jsCoq
The makefile shuffles some directories around because the root of the UniMath library is not the root of the repository, but one folder down. I am very much not an expert at these build processes, so if you know a better way to achieve the same (building the UniMath library with the root in the UniMath/UniMath folder, but in such a way that the build result ends up in the right spot etc), please let me know :-)
Arnoud van der Leer (Apr 14 2023 at 15:43):When I clone and make this project in a fresh directory on the same computer, it fails again with the same error.
Arnoud van der Leer (Apr 14 2023 at 15:57):I am not sure what is going wrong, partly because I am not entirely sure what software is coming from where.
At first, I got errors because I was (I believe) compiling with coq (and coq library) version 8.15.
Then I updated the package.json to require jscoq version 16, and then I got the errors because, apparently, I was compiling with coq 8.15against the library of version 8.16.
Can I infer from this that the jscoq package contains just the library? So where does the compiler come from? Is the compiler used that is installed centrally on my machine, or is jscoq also the compiler? That would make sense, since we are calling the jscoq npm package to start compilation. Or is there a docker container involved somewhere?
Shachar Itzhaky (Apr 16 2023 at 20:41):Yes @Arnoud van der Leer ; the Coq compiler is not portable and as such is not included in the NPM package.
I see that you are using the jsCoq SDK example. Did you follow the steps to clone and tag the Docker image? Perhaps you are right and we have overlooked this in 0.16.0 and did not place the correct version.
Another option for you would be to build jsCoq via the build instructions so that you have a compatible compiler. Then you run make install (make sure the jscoq switch is active so you do not overwrite your native version of Coq!) and compile the package normally without the SDK.
Arnoud van der Leer (Apr 17 2023 at 08:06):Hi. Thank you for the explanation. I ran make setup to download the dockerfile jscoq/jscoq:sdk, if that is what you meant. If it is not what you meant, can you explain where I can find the build instructions?
Arnoud van der Leer (Apr 17 2023 at 08:22):Ooooh, it is here, isn't it? https://github.com/jscoq/jscoq/tree/v8.16/etc/docker
Shachar Itzhaky (Apr 17 2023 at 17:39):Basically yes but building it retroactively to be compatible with the "official" NPM package is not that simple, I will have to check.
Arnoud van der Leer (Apr 17 2023 at 18:10):It works on my machine, I believe ^^
At least I don't get the error, currently.
Shachar Itzhaky (Apr 17 2023 at 18:11):yeah question is whether you will be able to compile your package with this new image
Shachar Itzhaky (Apr 17 2023 at 18:11):and whether it will co-operate with the jsCoq from NPM :) so many ifs
Arnoud van der Leer (Apr 17 2023 at 18:12):Hahaha. Well, at least it compiles (the first part of) my code again
Shachar Itzhaky (Apr 17 2023 at 18:12):good! the package building track still needs a lot of polishing and cleanup
Arnoud van der Leer (Apr 18 2023 at 08:17):It almost works, but on one file I am getting:
npx jscoq sdk dune build
coqc UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/EquivalenceWhiskeredNonCurriedMonoidalCategories.{glob,vo} (exit 129)
File "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/EquivalenceWhiskeredNonCurriedMonoidalCategories.v", line 333, characters 2-10:
Error: Anomaly "Uncaught exception Invalid_argument("String.create")."
Please report at http://coq.inria.fr/bugs/.
The internet suggests that this may be due to a very large proof term. I am however unsure where exactly this problem lies in the interaction between the unimath library and the jscoq sdk.
Shachar Itzhaky (Apr 18 2023 at 18:32):Oh wow debugging anomalies is super hard. @Emilio Jesús Gallego Arias any idea?
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:03):That's actually a quite strange one! If we look at the code raising the exn:
CAMLprim value caml_create_string(value len)
{
mlsize_t size = Long_val(len);
if (size > Bsize_wsize (Max_wosize) - 1){
caml_invalid_argument("String.create");
}
return caml_alloc_string(size);
}
where
#ifdef ARCH_SIXTYFOUR
#define Max_wosize (((intnat)1 << (54-PROFINFO_WIDTH)) - 1)
#else
#define Max_wosize ((1 << 22) - 1)
#endif /* ARCH_SIXTYFOUR */
could be actually the case that 32bit OCAML can't compile Unimath anymore? Typical value of PROFINFO_WITH is 0 when profiling is not enabled
I would just exclude that file @Arnoud van der Leer
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:07):Shachar Itzhaky said:
Oh wow debugging anomalies is super hard. Emilio Jesús Gallego Arias any idea?
You can call coqc with the -bt flag and get a backtrace, but the error seems to be indeed about Coq allocating some buffer larger than what the runtime allows, which given the line of the file in question could happen
Shachar Itzhaky (Apr 18 2023 at 19:07):Is there a string in UniMath that is larger than (1 << 22) - 1?
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:08):@Shachar Itzhaky no, but coqc allocates strings for a few things in Qed, for example to store the bytecode compiled version of Defined constants
Shachar Itzhaky (Apr 18 2023 at 19:08):oh..!
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:09):O_O
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:10):Yup that limit is pretty low in 32 bits!
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:10):Backtrace should tell us if that's the case
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:12):But surely it is this code actually:
let out_word env b1 b2 b3 b4 =
let p = env.out_position in
let buf =
let len = Bytes.length env.out_buffer in
if p + 3 < len then env.out_buffer
else
let new_len = min (Sys.max_string_length) (2 * len) in
(* Not the right exception... *)
let () = if not (p + 3 < new_len) then invalid_arg "String.create" in
let new_buffer = Bytes.create new_len in
let () = Bytes.blit env.out_buffer 0 new_buffer 0 len in
let () = env.out_buffer <- new_buffer in
new_buffer
in
let () = Bytes.set_uint8 buf p b1 in
let () = Bytes.set_uint8 buf (p + 1) b2 in
let () = Bytes.set_uint8 buf (p + 2) b3 in
let () = Bytes.set_uint8 buf (p + 3) b4 in
env.out_position <- p + 4
I don't see any other stuff in the Defined path that could cause this. I'm not surprised the definition in question takes more than 4 million ops in the Coq VM
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:15):Actually the limit is 4M words or 16MiB
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:15):[ballpark]
Emilio Jesús Gallego Arias (Apr 18 2023 at 19:46):Note the fixme haha "Not the right exception.." so indeed this should be replaced with a better error message.
Arnoud van der Leer (Apr 19 2023 at 06:18):Thank you for tracking the origin of the bug! So the conclusion is: UniMath is not suitable for compilation on 32 bits anymore?
In your experience, would it be possible to maybe break down this proof into smaller bits in order to compile it again on 32 bits?
And about this:
Emilio Jesús Gallego Arias said:
But surely it is this code actually:
let out_word env b1 b2 b3 b4 = ... env.out_position <- p + 4
Is this OCaml code of coq, or is it in UniMath somewhere?
Shachar Itzhaky (Apr 19 2023 at 08:25):This code is in Coq itself, but it is hard to tell which part of UniMath triggers the overflow. If you want to go deeper into it, try commenting out some of the proofs in the file until the error does not occur (sort of a binary search).
Arnoud van der Leer (Apr 22 2023 at 07:54):Okay, I split up the problematic definition, and now it works like a charm.
Arnoud van der Leer (Apr 22 2023 at 08:01):The next question is: is it possible to have an automatic build process? Is there a list of addons (https://github.com/jscoq/addons perhaps?) that are compiled automatically for new versions of jscoq and could we add the UniMath one to that list? Or should I set up a build process on the repository of the UniMath addon?
Shachar Itzhaky (Apr 22 2023 at 13:50):yes, we will be happy to add UniMath as a submodule
Shachar Itzhaky (Apr 22 2023 at 13:52):our automatic build does not use the SDK Docker (because it has some limitations, esp. handling package dependencies). But it should be possible to build it with your Dune files without Docker as well.
Arnoud van der Leer (Apr 22 2023 at 18:56):What are the changes that I would need to make? (Sidenote: The resulting package files end up in the /UniMath/_build folder instead of the /_build folder)
Arnoud van der Leer (Apr 26 2023 at 11:29):Or can you add UniMath as a submodule in its current state?
Shachar Itzhaky (Apr 27 2023 at 17:07):I will try, perhaps it will just work :)
Shachar Itzhaky (Apr 27 2023 at 17:11):it would help to have a short Coq script that imports UniMath and does a few basic things, as a smoke test
Arnoud van der Leer (Apr 27 2023 at 22:00):Ah, right. I will try to provide that :-)
Karl Palmskog (Apr 28 2023 at 06:42):I think there is some UniMath smoke test in the Coq Platform? May be worth checking Platform releases for that.
Shachar Itzhaky (Apr 28 2023 at 10:42):oh yes @Karl Palmskog I've been meaning to look at the various Coq smoke tests; these should also be useful for @Emilio Jesús Gallego Arias 's Coq-universe
Shachar Itzhaky (Apr 28 2023 at 12:59):@Arnoud van der Leer some of the files take a really long time to compile! Is that normal? I also tried compiling without the Docker and it still takes several minutes for some files, so the total time is well over an hour..!
Arnoud van der Leer (May 01 2023 at 06:45):Yeah, sorry, maybe should've warned you. I am not sure whether this is to be expected, but in its current state, the UniMath library takes a long time to compile.
Shachar Itzhaky (May 01 2023 at 08:19):ok np, I do have a server that I can use for releases, I'll just know to expect it :)
Arnoud van der Leer (May 09 2023 at 09:15):How is it going with this?
Arnoud van der Leer (May 09 2023 at 09:16):Can I help with something?
Shachar Itzhaky (May 09 2023 at 12:51):I have managed to compile your version, so if you have an example .v file that you managed to run on it I can use it to test whether it loads correctly.
Arnoud van der Leer (May 13 2023 at 11:24):Someone suggested testing it with
Require Import UniMath.All.
Check is_univalent.
Check @post_comp.
Could you do that? :-)
Shachar Itzhaky (May 14 2023 at 14:51):ok a bit lean but that's a start :)
Arnoud van der Leer (May 25 2023 at 14:55):Does it work? ^^
Shachar Itzhaky (May 28 2023 at 13:03):Hi sorry -- was working on a deadline and then we had a holiday here. But now I have some time to get back to it!
Arnoud van der Leer (May 29 2023 at 11:33):Hi! No problem, I haven't been particularly active either. Can I assist with something?
Shachar Itzhaky (May 29 2023 at 21:17):Screenshot-2023-05-30-at-0.14.38.png
Looks like it worked!
Shachar Itzhaky (May 29 2023 at 21:17):I had to make a few tweaks, to build it with my version instead of the Docker one. I think I will import your repo into the jscoq org and add you as a collaborator. Is this ok?
Arnoud van der Leer (May 30 2023 at 14:27):Yeah, sounds good!
Arnoud van der Leer (Jun 19 2023 at 12:40):Will this addon be bundled with the standard version of jscoq? (e.g. https://coq.vercel.app/scratchpad.html)
Arnoud van der Leer (Jun 21 2023 at 14:31):And/or is there a good way / do you have a good way to have github build a new version of the addon every time the unimath codebase is updated?
Shachar Itzhaky (Jun 21 2023 at 14:42):yes we are definitely going to add it to the 8.17 release which we did not have the time to stabilize
Shachar Itzhaky (Jun 21 2023 at 14:43):as for continuous updates, when we create a jsCoq release we usually try to update the addons but it's pretty manual
Arnoud van der Leer (Jun 22 2023 at 11:51):Ah, okay. Thanks!
Arnoud van der Leer (Jun 27 2023 at 17:22):I also set up a version on our github pages: https://unimath.github.io/live/
(https://github.com/UniMath/live/blob/master/index.html)
However, when I set coq: {'Universe Checking': false}, it breaks down. Any idea what may be the problem?
Emilio Jesús Gallego Arias (Jun 28 2023 at 09:09):Cool @Arnoud van der Leer , what does "break down" mean?
Emilio Jesús Gallego Arias (Jun 28 2023 at 09:10):Do you have some log / console output?
Arnoud van der Leer (Jun 28 2023 at 10:33):Anomaly ""Assert_failure _vendor+v8.16+32bit/coq/library/lib.ml:169:57"."
Please report at http://coq.inria.fr/bugs/.
Anomaly "Uncaught exception Option.IsNone."
Please report at http://coq.inria.fr/bugs/.
Or in the chrome console:
image.png
(This is the default examples/scatchpad.html, to which I added the option coq: {'Implicit Arguments': true, 'Default Timeout': 10})
Emilio Jesús Gallego Arias (Jun 28 2023 at 14:17):I know what the problem is, we set the option before the Coq library is initialized
Emilio Jesús Gallego Arias (Jun 28 2023 at 14:17):I think
Emilio Jesús Gallego Arias (Jun 28 2023 at 14:17):Please @Arnoud van der Leer can you open a bug so keep track of this problem?
Emilio Jesús Gallego Arias (Jun 28 2023 at 14:19):Thanks for the debug info, it was very important
Arnoud van der Leer (Aug 14 2023 at 13:12):Please Arnoud van der Leer can you open a bug so keep track of this problem?
Do you want me to open a bug at coq.inria, or at the jsCoq GitHub?
Shachar Itzhaky (Aug 14 2023 at 15:28):It seems more appropriate for jsCoq
Arnoud van der Leer (Aug 15 2023 at 08:52):I filed an issue on GitHub
Julien Narboux (Sep 01 2023 at 15:18):Hi, we would like to create a jsCoq package for GeoCoq. We are trying to use the approach based on the Docker sdk.
When I try :
npx jscoq sdk coqc -v
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.12.0
Is it normal ? I thought current version was 8.17.
I tried the Group-theory example, it went up to the point: wrote coq-pkgs/group-theory.coq-pkg.
But running npx http-serve sdk-demo/ I get:
Capture-décran-2023-09-01-à-15.57.27.png
Shachar Itzhaky (Sep 05 2023 at 12:27):oh, it looks like this fell into disuse. I have to upload new versions of the SDK -- this should be incorporated into our release cycle.
Shachar Itzhaky (Sep 05 2023 at 22:08):I have updated the sdk. We will have sdk tags include the version number from now on, and also have an alias jscoq/jscoq:sdk pointing to the latest one.
I have also updated the NPM packages for 0.17.0.
Julien Narboux (Sep 27 2023 at 08:28):Shachar Itzhaky said:
I have updated the sdk. We will have sdk tags include the version number from now on, and also have an alias jscoq/jscoq:sdk pointing to the latest one.
I have also updated the NPM packages for 0.17.0.
Thanks. Last week we gave a tutorial using jscoq, but on some browsers/systems it was not working at all, and on some other we had some stack overflow. So I would like to try web assembly version.
I tried to run make wabuild in etc/docker and I obtain the following error.
=> ERROR [wacoq-prereq 2/7] RUN git clone --recursive -b 2.3s
------
> [wacoq-prereq 2/7] RUN git clone --recursive -b v8.17 https://github.com/jscoq/wacoq-bin.git wacoq-bin:
#15 1.109 Cloning into 'wacoq-bin'...
#15 2.175 fatal: Remote branch v8.17 not found in upstream origin
------
executor failed running [/bin/sh -c git clone --recursive -b ${WACOQ_BIN_BRANCH} ${WACOQ_BIN_REPO} wacoq-bin]: exit code: 128
make: *** [wa-build-core] Error 1 ```
hi
wacoq-bin is discontinued since we have unified the backends. This should be evicted from the Makefile. make js-build should build both now actually.
Arnoud van der Leer (Oct 27 2023 at 13:36):Hi. I am trying to build a plugin on a fresh Ubuntu install. These are the current steps:
# Install applications
sudo apt update
sudo apt install git make docker.io opam
# The newest version of nodejs is not available via apt, so we need to install it via snap
snap install node --classic
# Dune is available via the opam package manager
opam init
opam install dune coq # Not sure whether coq is necessary
# Make sure that docker has the right permissions. See for example https://phoenixnap.com/kb/docker-permission-denied
sudo groupadd -f docker
sudo usermod -aG docker $USER
newgrp docker
# Build the plugin itself
git clone https://github.com/UniMath/UniMath-jsCoq.git
cd UniMath-jsCoq
make setup
make
However, when I do this, I get
npx jscoq sdk dune build --root UniMath
Entering directory '..../UniMath-jsCoq/UniMath'
Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version.
Command exited with code 1.
-> required by alias default
make: *** [Makefile:10: build] Error 1
Is there a way to find out what is going wrong?
Emilio Jesús Gallego Arias (Oct 27 2023 at 21:14):Hi @Arnoud van der Leer , try dune build --display=verbose to get more information?
Arnoud van der Leer (Oct 28 2023 at 09:24):Then I get
# Use current workspace, not jsCoq's
(cd UniMath ; git pull)
Already up to date.
npx jscoq sdk dune build --display=verbose --root UniMath
Entering directory '/home/arnoud/UniMath-jsCoq/UniMath'
Shared cache: disabled
Workspace root: /home/arnoud/UniMath-jsCoq/UniMath
Auto-detected concurrency: 1
Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
3.8 and will be removed in an upcoming Dune version.
Dune context:
{ name = "default"
; kind = "default"
; profile = Dev
; merlin = true
; for_host = None
; fdo_target_exe = None
; build_dir = In_build_dir "default"
; ocaml_bin = External "/usr/bin"
; ocaml = Ok External "/usr/bin/ocaml"
; ocamlc = External "/usr/bin/ocamlc.opt"
; ocamlopt = Ok External "/usr/bin/ocamlopt.opt"
; ocamldep = Ok External "/usr/bin/ocamldep.opt"
; ocamlmklib = Ok External "/usr/bin/ocamlmklib.opt"
; installed_env =
map
{ "INSIDE_DUNE" : "/home/arnoud/UniMath-jsCoq/UniMath/_build/default"
; "OCAML_COLOR" : "always"
; "OPAMCOLOR" : "always"
}
; findlib_paths = [ External "/home/arnoud/.opam/default/lib" ]
; ocaml_config =
{ version = "4.13.1"
; standard_library_default = "/usr/lib/ocaml"
; standard_library = "/usr/lib/ocaml"
; standard_runtime = "the_standard_runtime_variable_was_deleted"
; ccomp_type = "cc"
; c_compiler = "x86_64-linux-gnu-gcc"
; ocamlc_cflags =
[ "-O2"
; "-fno-strict-aliasing"
; "-fwrapv"
; "-pthread"
; "-fPIC"
; "-g"
; "-O2"
; "-ffile-prefix-map=/build/ocaml-SC7b9w/ocaml-4.13.1=."
; "-fstack-protector-strong"
; "-Wformat"
; "-Werror=format-security"
]
; ocamlc_cppflags =
[ "-D_FILE_OFFSET_BITS=64"; "-Wdate-time"; "-D_FORTIFY_SOURCE=2" ]
; ocamlopt_cflags =
[ "-O2"
; "-fno-strict-aliasing"
; "-fwrapv"
; "-pthread"
; "-fPIC"
; "-g"
; "-O2"
; "-ffile-prefix-map=/build/ocaml-SC7b9w/ocaml-4.13.1=."
; "-fstack-protector-strong"
; "-Wformat"
; "-Werror=format-security"
]
; ocamlopt_cppflags =
[ "-D_FILE_OFFSET_BITS=64"; "-Wdate-time"; "-D_FORTIFY_SOURCE=2" ]
; bytecomp_c_compiler =
[ "x86_64-linux-gnu-gcc"
; "-O2"
; "-fno-strict-aliasing"
; "-fwrapv"
; "-pthread"
; "-fPIC"
; "-g"
; "-O2"
; "-ffile-prefix-map=/build/ocaml-SC7b9w/ocaml-4.13.1=."
; "-fstack-protector-strong"
; "-Wformat"
; "-Werror=format-security"
; "-D_FILE_OFFSET_BITS=64"
; "-Wdate-time"
; "-D_FORTIFY_SOURCE=2"
]
; bytecomp_c_libraries = [ "-lm"; "-lpthread" ]
; native_c_compiler =
[ "x86_64-linux-gnu-gcc"
; "-O2"
; "-fno-strict-aliasing"
; "-fwrapv"
; "-pthread"
; "-fPIC"
; "-g"
; "-O2"
; "-ffile-prefix-map=/build/ocaml-SC7b9w/ocaml-4.13.1=."
; "-fstack-protector-strong"
; "-Wformat"
; "-Werror=format-security"
; "-D_FILE_OFFSET_BITS=64"
; "-Wdate-time"
; "-D_FORTIFY_SOURCE=2"
]
; native_c_libraries = [ "-lm" ]
; native_pack_linker = [ "x86_64-linux-gnu-ld"; "-r"; "-o" ]
; cc_profile = []
; architecture = "amd64"
; model = "default"
; int_size = 63
; word_size = 64
; system = "linux"
; asm = [ "x86_64-linux-gnu-as" ]
; asm_cfi_supported = true
; with_frame_pointers = false
; ext_exe = ""
; ext_obj = ".o"
; ext_asm = ".s"
; ext_lib = ".a"
; ext_dll = ".so"
; os_type = "Unix"
; default_executable_name = "a.out"
; systhread_supported = true
; host = "x86_64-pc-linux-gnu"
; target = "x86_64-pc-linux-gnu"
; profiling = false
; flambda = false
; spacetime = false
; safe_string = true
; exec_magic_number = "Caml1999X030"
; cmi_magic_number = "Caml1999I030"
; cmo_magic_number = "Caml1999O030"
; cma_magic_number = "Caml1999A030"
; cmx_magic_number = "Caml1999Y030"
; cmxa_magic_number = "Caml1999Z030"
; ast_impl_magic_number = "Caml1999M030"
; ast_intf_magic_number = "Caml1999N030"
; cmxs_magic_number = "Caml1999D030"
; cmt_magic_number = "Caml1999T030"
; natdynlink_supported = true
; supports_shared_libraries = true
; windows_unicode = false
}
; instrument_with = []
}
Actual targets:
- alias @@default
Command exited with code 1.
-> required by alias default
make: *** [Makefile:10: build] Error 1
When running, it stays at the following for about a second, before replacing it with the Command exited with code 1.:
Done: 0% (12/2256, 2244 left) (jobs: 1)
That's pretty strange, but I've seen it before; I dont' recall what it was.
Arnoud van der Leer (Oct 28 2023 at 18:06):Oh, that is unfortunate. Do you have any advice? Note: this was on a fresh ubuntu install (VM), so no "additional" software or packages were present.
Emilio Jesús Gallego Arias (Oct 29 2023 at 22:04):Indeed it is really unfortunate @Arnoud van der Leer ; I'd love to debug this myself, but as of today we have 0 developer time assigned to jsCoq :(
Arnoud van der Leer (Oct 30 2023 at 06:49):Ah, that sucks. Thank you for your answers at least.
Emilio Jesús Gallego Arias (Oct 30 2023 at 11:29):I'm indeed sorry, trying to find out some help.
Does Unimath build OK without the npx stuff?
Emilio Jesús Gallego Arias (Oct 30 2023 at 11:30):I had seen that error in the past, however it was when OCaml wasn't ready.
Actually I have a suggestion, can you try to build again with Dune 3.7.1 ?
Emilio Jesús Gallego Arias (Oct 30 2023 at 11:31):This could be a bug in Dune 3.8
Arnoud van der Leer (Oct 30 2023 at 14:16):So I was working with Dune 3.11. When I downgraded to 3.7.1 and tried to build the plugin again, I got
# Use current workspace, not jsCoq's
(cd UniMath ; git pull)
Already up to date.
npx jscoq sdk dune build --root UniMath
Entering directory '/home/arnoud/UniMath-jsCoq/UniMath'
File "UniMath/dune", line 4, characters 0-164:
4 | (coq.theory
5 | (name UniMath)
6 | (package coq-unimath)
7 | (flags :standard
8 | -noinit
9 | -indices-matter
10 | -type-in-type
11 | -w -notation-overridden))
Command exited with code 1.
make: *** [Makefile:10: build] Error 1
Which is different, but not better, I guess.
Last updated: Dec 07 2023 at 17:01 UTC