Vojtěch Štěpančík (Mar 12 2022 at 19:01): Vojtěch Štěpančík (Mar 12 2022 at 19:01):Hello, sorry for the incoming wall of text - I hope it doesn't sound rambly, I very much appreciate what jsCoq does for making Coq development more accessible, but I can't for the love of me figure out how to make it do exactly what I want.
Vojtěch Štěpančík (Mar 12 2022 at 19:02):I'm trying to put together an environment for writing a textbook for an undergraduate logic course. Because we want the textbook to be interactive, it will be a website with jsCoq integrated, so that the students can step through the proofs and solve exercises directly in the textbook.
I have an almost-working setup that I will describe in the following lines, but I think it's a little clunky and over-engineered, so I'd appreciate any feedback on where I might have taken a wrong turn. I don't think doing what I want should be that difficult :).
We want the textbook to be split into chapters, where each chapter is its own webpage, but it can still depend on theorems from preceding chapters. After going through the docs, I came to the conclusion that I want to pre-compile all the Coq files, and package them in a .coq-pkg.
However I can't figure out how to use the .vo files for Coq's stdlib that are already compiled on my system - I see that jscoq's coq-pkgs Dune target calls the CLI on the local checkout of Coq's sources, but the directory structure is different from what I have when I install Coq: specifically the plugins have different names - in Coq source, there's a plugins/syntax directory, but I have lib/coq-core/plugins/{float_syntax,number_string_notation}, which I guess are somehow "inside out", because they are actually the targets that Dune builds when it builds the plugins/syntax directory (I'm not exactly sure how this works or what the vocabulary is, I only saw Dune builds yesterday).
Because of this difference, jscoq complains during packaging of the .coq-pkg, because it can't find the directory plugins/syntax, which is specified in jscoq/coq-jslib/metadata/coq-pkgs.json, and that's the furthest I've gotten.
Where do I go from here? I would like to avoid installing Opam, Dune, and building Coq from source from the ground up, because I want to make it user-friendly for other people that will be writing the textbook.
Vojtěch Štěpančík (Mar 12 2022 at 19:06):(an alternative I considered was to just include the source of all the preceding chapters as a hidden element on every page, and letting jsCoq reinterpret everything, but the used-to-be web engineer in me shivers at the thought of the wasted computing power and bandwidth :smiley:)
Vojtěch Štěpančík (Mar 12 2022 at 19:57):Hm, now that I'm taking a closer look at how building works - is it possible that I simply can't avoid building Coq from source? Since I see now that jsCoq applies some patches to Coq's source?
Emilio Jesús Gallego Arias (Mar 14 2022 at 13:14):Hi @Vojtěch Štěpančík , your input is appreciated and indeed it doesn't sound rambly at all!
Emilio Jesús Gallego Arias (Mar 14 2022 at 13:15):We are sorry the workflow we have for this is really bad, as you had to suffer, we have plans to much improve it. But indeed, as of today, you are correct that unfortunately Coq doesn't provide binary compatibility for .vo files, so you need to compile them using the same Coq version that jsCoq is using. We hope to fix this soon. @Shachar Itzhaky once had a mode where you could compile them.
Emilio Jesús Gallego Arias (Mar 14 2022 at 13:17):You have two choices as of today, both of them are not very good:
Shachar Itzhaky (Mar 14 2022 at 13:56):Hi @Vojtěch Štěpančík; you will need to compile the same version of Coq that jsCoq is using, esp. it has to be 32-bit (which is what Web environments provide atm).
Please follow this doc: https://github.com/jscoq/jscoq/blob/v8.14/docs/build.md
Vojtěch Štěpančík (Mar 14 2022 at 14:26):Ok, thanks for the info - I'll look into the Docker setup, and see if I can integrate it properly into our CI pipeline - I'm currently managing the build with Nix, so I might have to write a derivation for jsCoq, as I haven't seen any
Shachar Itzhaky (Mar 14 2022 at 14:42):Oh interesting! I did try to use Nix some time ago and did not manage to make it work :D If you make progress with it do let us know.
Karl Palmskog (Mar 14 2022 at 15:15):@Vojtěch Štěpančík for any Nix+Coq applications, we recommend: https://github.com/coq-community/coq-nix-toolbox
Vojtěch Štěpančík (Mar 14 2022 at 15:16):Karl Palmskog said:
Vojtěch Štěpančík for any Nix+Coq applications, we recommend: https://github.com/coq-community/coq-nix-toolbox
Thanks! I'll take a look
Shachar Itzhaky (Mar 14 2022 at 17:16):Thanks @Karl Palmskog; I managed to run the installation scripts from coq-nix-toolbox. Nice! This is the first time I actually ran something in a Nix environment and it worked.
Karl Palmskog (Mar 14 2022 at 17:37):Note that there is a dedicated stream to the Nix toolbox: #Nix toolbox devs & users
Vojtěch Štěpančík (Mar 15 2022 at 22:15):I feel like I'm this 🤏 close to getting it working - I can't really use the mentioned Nix toolbox I think, because IIUC it's for building Coq packages, and what I'm doing here is building Coq and jsCoq, neither of which are Coq packages.
I managed to build Coq, the jsCoq CLI, and package the Coq stdlib into .coq-pkg files, but I'm stuck on building jscoq_worker. When running dune build @jscoq_worker, I get an error about a missing implementation:
bash-5.1$ dune build @jscoq_worker
File "_none_", line 1:
Error: No implementations provided for the following modules:
Migrate_parsetree__Migrate_parsetree_versions referenced from /nix/store/kmxwyw4is2hmyfq3rs0sfxbr6prw5p1v-ocaml4.12.0-ppx_import-1.8.0/lib/ocaml/4.12.0/site-lib/ppx_import/ppx_import.cmxa(Ppx_import__Ppx_types_migrate),
/nix/store/kmxwyw4is2hmyfq3rs0sfxbr6prw5p1v-ocaml4.12.0-ppx_import-1.8.0/lib/ocaml/4.12.0/site-lib/ppx_import/ppx_import.cmxa(Ppx_import)
Migrate_parsetree__Migrate_parsetree_driver referenced from /nix/store/kmxwyw4is2hmyfq3rs0sfxbr6prw5p1v-ocaml4.12.0-ppx_import-1.8.0/lib/ocaml/4.12.0/site-lib/ppx_import/ppx_import.cmxa(Ppx_import)
I'm trying to have my OCaml dependencies managed by Nix instead of ocaml, so I changed (opam (switch jscoq+32bit) ...) to (default ...) - could that be a problem? I'm not sure what that would change, I'd assume it would just not use opam for managing external dependencies.
Has anyone encountered this error before? I'm not having any luck ddg'ing it, and I'm new to the whole OCaml ecosystem.
Vojtěch Štěpančík (Mar 15 2022 at 22:29):Oh, that seems to be some Nix x Ocamlfind interaction, so it's a me-problem https://discourse.nixos.org/t/issue-building-ocaml-project/13739
Shachar Itzhaky (Mar 16 2022 at 13:37):Vojtěch Štěpančík said:
Oh, that seems to be some Nix x Ocamlfind interaction, so it's a me-problem https://discourse.nixos.org/t/issue-building-ocaml-project/13739
A very curious symptom at that... did you manage to overcome it?
I am pretty sure you do need to compile within the jscoq+32bit switch, otherwise you will get a 64-bit binary.
Vojtěch Štěpančík (Mar 16 2022 at 16:50):I wouldn't get a 64bit binary, since I was using the i686-linux package set - I haven't played with it since I wrote that message, but I think I'll probably start over, delegating everything except source fetching, node_modules fetching, and preferably OCaml package fetching to dune; I think the problem is that Nix allows multiple versions of the same library to exist, and I was getting different versions of migrate-parsetree in OCAMLPATH, so if I figure out how to set everything to only one version, it should be fine
Vojtěch Štěpančík (Mar 16 2022 at 16:51):I was probably getting too fancy with it, I tried splitting the Coq and jsCoq derivations, but I don't think it's worth it anymore
Shachar Itzhaky (Mar 16 2022 at 21:29):Oh sure, if you are using an i686 distro then you're probably ok using the default switch. But I see no reason not to use the jscoq+32bit switch anyway, and it should work just as well.
Vojtěch Štěpančík (Mar 16 2022 at 22:12):Well, I'm not using an i686 distro, I'm just using legacyPackages.i686-linux from the nixpkgs flake, so that I get 32bit a OCaml compiler - that's equivalent to using the jscoq+32bit switch, no?
Shachar Itzhaky (Mar 19 2022 at 21:50):Yes, that sounds reasonable. Did you manage to find a solution?
Vojtěch Štěpančík (Mar 19 2022 at 22:57):Almost there - I had to rewrite it a few times, but now I've reached a state (now ~ the build finished 20mins ago) where I have a Nix package for jsCoq, which also exposes the Coq version that's used internally, and now I'm testing it; coqc seems to work, except I have to pass -coqlib manually, so I'll have to look into that
Vojtěch Štěpančík (Mar 20 2022 at 10:59):So I fixed that by changing the prefix and libdir configuration parameters, but now coq_makefile is acting up
Vojtěch Štěpančík (Mar 20 2022 at 11:02):It can't find CoqMakefile.in unless I specify COQCORELIB explicitly, which is weird - if I'm reading the source for coq_makefile and lib/envars correctly, it should infer it by guessing the coqlib directory, and then going ../coq-core/
Vojtěch Štěpančík (Mar 20 2022 at 11:03):I have the directories coq and coq-core right beside each other, but it still can't find coq-core
Vojtěch Štěpančík (Mar 20 2022 at 11:04):Even when I specify COQLIB, which should eliminate any guessing
Vojtěch Štěpančík (Mar 20 2022 at 11:04):(btw is this still the right place to write this, or should I move somewhere else?)
Vojtěch Štěpančík (Mar 20 2022 at 11:11):Oh shoot, never mind, it seems like I was experimenting too much in the terminal and ended up doing export COQCORELIB=.../coq, no wonder the resolution was all messed up, after restarting the shell coq_makefile works :ok:
Vojtěch Štěpančík (Mar 20 2022 at 11:22):Everything's working, I can finally build and deploy my .v files and load them in jsCoq :tada:
Vojtěch Štěpančík (Mar 20 2022 at 11:23):I'll clean up the Nix file, write some docs, and push it on GitHub
Shachar Itzhaky (Mar 20 2022 at 19:28):Sweet! We will be happy to put it up on our GitHub as well. For sure we will link to it from our website.
Vojtěch Štěpančík (Mar 21 2022 at 00:45):All right, I published the thingy on GitHub, it includes some docs and a template for getting started. I tested it on my machine, and both 32bit and 64bit Linux systems should be supported. I don't have a Mac to test it on darwin, so it contains only Linux outputs for now. Unfortunately, a cold build takes quite some time, since the OCaml packages need to be rebuilt, and there is no i686 binary cache for nixpkgs (so I think at some point I was even compiling glibc and gcc...). Anyway, feel free to give me feedback, and link the repo where you deem appopriate https://github.com/VojtechStep/jscoq-nix
Shachar Itzhaky (Mar 21 2022 at 20:51):Nix flake... oh I have so much more to learn :)
Vojtěch Štěpančík (Mar 21 2022 at 22:02):I just added materialization (the previous version had ocaml and other stuff as eval dependencies, now its result is cached and stored in a json file, so they aren't necessary anymore) and I set up a binary cache (instructions are in the readme), so now nothing should have to be compiled locally, everything is downloaded
Théo Zimmermann (Mar 22 2022 at 08:34):Shachar Itzhaky said:
Nix flake... oh I have so much more to learn :smile:
Actually me too :smile: I'm an old Nix user now (~6 years) using the stable CLI and postponing the moment where I will learn about all the new shiny experimental features.
Last updated: Jun 01 2023 at 12:01 UTC