Stream: jsCoq

Topic: Rules for .coq-pkg


view this post on Zulip 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} ....)))

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 15:52):

So what are the actual parameters that the (run invocation does need?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 15:53):

Dune already has full knowledge of modules, deps, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 15:53):

And can have coq-pkg avoid any filesystem scanning if we want it

view this post on Zulip Shachar Itzhaky (Apr 08 2021 at 15:53):

I assume %{bin:coq-pkg} is npx jscoq or smt similar?

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Apr 08 2021 at 15:54):

i.e. logical and physical paths

view this post on Zulip Shachar Itzhaky (Apr 08 2021 at 15:54):

let me send you an example

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 15:54):

That'd be fine, Dune could build that file and pass it

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Apr 08 2021 at 15:57):

https://github.com/jscoq/addon-elpi/blob/d6867878738cd949d9eddabd0e49cbb744ec250c/elpi.json

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Shachar Itzhaky (Apr 08 2021 at 16:00):

It does not compile .v to .vo. This is done by Dune already.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 16:00):

Ah so it only scans the files

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 16:01):

yes that is PITA

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Apr 08 2021 at 19:25):

exciting!


Last updated: Jan 30 2023 at 18:04 UTC