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.
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
Here is the HoTT library for example: https://x80.org/rhino-hott/
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.
cc @Emilio Jesús Gallego Arias
"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
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.
@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.
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.
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.
@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.
@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.
I guess I would just start from some of the addons in https://github.com/jscoq/ and do unitmath that way
Thanks, I'll take a look!
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?
(So which version of coq handles the npx jscoq sdk dune build
command?)
Hi @Arnoud van der Leer , npx jscoq will likely pick Coq 8.16 as it is the latest available in npm
Indeed the problem seems that the unimath version may not be compatible with 8.16?
Well, actually UniMath compiles fine on my machine with version 8.16
Is there a way to check or force which version of coq it is compiling against?
Yes, using npm exec --package=<pkg>@version -- cmd
should do the trick as to pick the right jscoq version
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
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.
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?
Yes, somehow you are calling Coq 8.15 with a 8.16 library
Maybe you can try open an issue in the jsCoq repos outlining all the steps you've done from the start?
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 :-)
When I clone and make this project in a fresh directory on the same computer, it fails again with the same error.
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.15
against 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 that the dockerfile? Is it possible that that one is outdated then?
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.
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?
Ooooh, it is here, isn't it? https://github.com/jscoq/jscoq/tree/v8.16/etc/docker
Basically yes but building it retroactively to be compatible with the "official" NPM package is not that simple, I will have to check.
It works on my machine, I believe ^^
At least I don't get the error, currently.
yeah question is whether you will be able to compile your package with this new image
and whether it will co-operate with the jsCoq from NPM :) so many ifs
Hahaha. Well, at least it compiles (the first part of) my code again
good! the package building track still needs a lot of polishing and cleanup
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.
Oh wow debugging anomalies is super hard. @Emilio Jesús Gallego Arias any idea?
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
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
Is there a string in UniMath that is larger than (1 << 22) - 1
?
@Shachar Itzhaky no, but coqc allocates strings for a few things in Qed, for example to store the bytecode compiled version of Defined constants
oh..!
O_O
Yup that limit is pretty low in 32 bits!
Backtrace should tell us if that's the case
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
Actually the limit is 4M words or 16MiB
[ballpark]
Note the fixme haha "Not the right exception.." so indeed this should be replaced with a better error message.
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?
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).
Okay, I split up the problematic definition, and now it works like a charm.
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?
yes, we will be happy to add UniMath as a submodule
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.
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)
Or can you add UniMath as a submodule in its current state?
I will try, perhaps it will just work :)
it would help to have a short Coq script that imports UniMath and does a few basic things, as a smoke test
Ah, right. I will try to provide that :-)
I think there is some UniMath smoke test in the Coq Platform? May be worth checking Platform releases for that.
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
@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..!
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.
ok np, I do have a server that I can use for releases, I'll just know to expect it :)
How is it going with this?
Can I help with something?
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.
Someone suggested testing it with
Require Import UniMath.All.
Check is_univalent.
Check @post_comp.
Could you do that? :-)
ok a bit lean but that's a start :)
Does it work? ^^
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!
Hi! No problem, I haven't been particularly active either. Can I assist with something?
Screenshot-2023-05-30-at-0.14.38.png
Looks like it worked!
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?
Yeah, sounds good!
Last updated: Jun 10 2023 at 06:31 UTC