Emilio Jesús Gallego Arias (Apr 08 2021 at 15:52): Emilio Jesús Gallego Arias (Apr 08 2021 at 15:52):Hi @Shachar Itzhaky , I'd like to add a built-in rule to Dune's Coq rules so we can just do:
$ dune build mathcomp.algebra.coq-pkg
and have the things work properly, the rule is very simple, and of the form:
(rule
(targets $lib.coq-pkg)
(deps (:modules $all_vo_of_lib))
(action (run %{bin:coq-pkg} ....)))
So what are the actual parameters that the (run invocation does need?
Emilio Jesús Gallego Arias (Apr 08 2021 at 15:53):Dune already has full knowledge of modules, deps, etc...
Emilio Jesús Gallego Arias (Apr 08 2021 at 15:53):And can have coq-pkg avoid any filesystem scanning if we want it
Shachar Itzhaky (Apr 08 2021 at 15:53):I assume %{bin:coq-pkg} is npx jscoq or smt similar?
Emilio Jesús Gallego Arias (Apr 08 2021 at 15:54):Yes, that's the idea, your tool is super useful in other context [such as windows users]
Emilio Jesús Gallego Arias (Apr 08 2021 at 15:54):so the idea is to make that tool at some into the official Coq distribution
Shachar Itzhaky (Apr 08 2021 at 15:54):So the way it currently works is you can pass it a JSON file with the list of packages
Shachar Itzhaky (Apr 08 2021 at 15:54):i.e. logical and physical paths
Shachar Itzhaky (Apr 08 2021 at 15:54):let me send you an example
Emilio Jesús Gallego Arias (Apr 08 2021 at 15:54):That'd be fine, Dune could build that file and pass it
Emilio Jesús Gallego Arias (Apr 08 2021 at 15:55):One point is plugins, indeed the final package format may want to have plugins in a bit of a different way, likely as optional sections inside the coq-pkg file, as Coq is moving towards handling plugins using the OCaml namespace. Maybe that's not a super good choice.
Shachar Itzhaky (Apr 08 2021 at 15:57):https://github.com/jscoq/addon-elpi/blob/d6867878738cd949d9eddabd0e49cbb744ec250c/elpi.json
Shachar Itzhaky (Apr 08 2021 at 15:58):Yeah the current tool is pretty hard-wired to find bytecode files (and optionally run them through js_of_ocaml).
Shachar Itzhaky (Apr 08 2021 at 15:59):The JSON format is a bit spartan, I initially made it as some internal thing for us, perhaps we should rethink it if we expect people to actually use the packager. Unless they only use it from Dune and then they never have to see the JSON.
Emilio Jesús Gallego Arias (Apr 08 2021 at 15:59):So what does the tool do now exactly? I assume it does something like:
I'd like to delegate maybe 1 and 2 to dune.
Emilio Jesús Gallego Arias (Apr 08 2021 at 16:00):The JSON format is a bit spartan, I initially made it as some internal thing for us, perhaps we should rethink it if we expect people to actually use the packager. Unless they only use it from Dune and then they never have to see the JSON.
I don't mind either option, for now it is just an internal thing, I guess we could do without the json and just use command line arguments --buildir etc...
Shachar Itzhaky (Apr 08 2021 at 16:00):It does not compile .v to .vo. This is done by Dune already.
Emilio Jesús Gallego Arias (Apr 08 2021 at 16:00):Ah so it only scans the files
Shachar Itzhaky (Apr 08 2021 at 16:00):It only compiles .cma -> .cma.js because it was a hassle for me to do it in Dune.
Emilio Jesús Gallego Arias (Apr 08 2021 at 16:01):yes that is PITA
Shachar Itzhaky (Apr 08 2021 at 16:02):The command-line options don't give you full control, you can only specify a root and then it will collect all the modules from there, but you cannot pick specific dirpaths like in the JSON.
Shachar Itzhaky (Apr 08 2021 at 16:02):But yeah if that works in your case you can infer the root dir and pass it.
Shachar Itzhaky (Apr 08 2021 at 16:04):It puts .vo files that it has located in the .coq-pkg. If it also finds .v, then it runs coqdep on them (actually a clone of coqdep that I wrote in JS some time ago...) to infer inter-module dependencies. It can create the package from compiled files only, but then you won't have autoloaded deps.
Emilio Jesús Gallego Arias (Apr 08 2021 at 16:06):Dune has already ran coqdep on all the files so it just needs to pass to the tool the output; what format would be best?
Shachar Itzhaky (Apr 08 2021 at 16:10):I just had the same thought. Actually dune has done all the work already. .coq-pkg is simply a zip file with a manifest. If you have the dep info then you have essentially generated the manifest, you just have to add it to the zip. Look in _build/jscoq+32bit/coq-pkgs/coq.json to see how it's constructed.
Emilio Jesús Gallego Arias (Apr 08 2021 at 18:12):Thanks for the info; so maybe we could have coqdep directly outputting that format I think.
Emilio Jesús Gallego Arias (Apr 08 2021 at 18:12):We are actually pretty close to merging the coqdep refactoring which was promised some time ago
Shachar Itzhaky (Apr 08 2021 at 19:25):exciting!
Last updated: Jun 01 2023 at 12:01 UTC