Stream: jsCoq

Topic: How to create a version of jsCoq with more packages?

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 that the dockerfile? Is it possible that that one is outdated then?

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 */

Emilio Jesús Gallego Arias (Apr 18 2023 at 19:05):

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!

Last updated: Jun 10 2023 at 06:31 UTC