Stream: math-comp devs

Topic: hierarchy.ml


view this post on Zulip Pierre-Yves Strub (May 19 2020 at 08:09):

Hi. How should I use utils/hierarchy.ml for checking my hierarchy? I am currently modifying order.v and I screw a join somewhere and I'd like to use that tool to point me in the right direction.

view this post on Zulip Kazuhiko Sakaguchi (May 19 2020 at 08:14):

In MathComp, make test-suite lets you run hierarchy.ml properly.

view this post on Zulip Kazuhiko Sakaguchi (May 19 2020 at 08:20):

But it requires all/all.vo and thus has to compiles MathComp entirely.

view this post on Zulip Emilio Jesús Gallego Arias (May 19 2020 at 12:19):

By the way @Kazuhiko Sakaguchi , wouldn't it easier for hiearchy.ml to be written against Coq's ML API? That would make some of the code quite a bit more robust. [I could help but not this week, very short on cycles these days]

view this post on Zulip Enrico Tassi (May 19 2020 at 14:16):

Note that we test the very same MC commit against many Coq versions, not very easy to handle in the usual Coq workflow if the the API changes.

view this post on Zulip Pierre-Yves Strub (May 19 2020 at 14:32):

Ok, I adapted the Makefile rule to my needs -- because compiling mathcomp each time if want to check a file won't do it.

view this post on Zulip Pierre-Yves Strub (May 20 2020 at 06:28):

The script should not pass an empty environment to open_process_full (this totally destroys the settings of opam). It should preserve the parent process environment by passing Unix.environment ().

view this post on Zulip Pierre-Yves Strub (May 20 2020 at 06:31):

Anyway, from master, after having fixed that and compiled order.v (unmodified), I run:

ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib ssreflect.order > check.v

I obtain a big file with a lot of checks, but it doesn't work

➜  coqc -I . -R . mathcomp check.v
File "./check.v", line 30, characters 34-39:
Error:
The term "Order.CBDistrLattice.class (id (?t : cbDistrLatticeType ?d1))"
has type "Order.CBDistrLattice.class_of (id ?t)"
while it is expected to have type "Type".

view this post on Zulip Pierre-Yves Strub (May 20 2020 at 06:34):

(Also, the script should check the exit status of coqtop. Each time a syscall return code is ignored, a kitty dies)

view this post on Zulip Karl Palmskog (May 26 2020 at 15:57):

wouldn't it make sense to actually compile and package hierarchy.ml as a regular program in (Coq's) OPAM @Kazuhiko Sakaguchi? It seems inconvenient to use ocaml as above and pinpoint the file every time

view this post on Zulip Karl Palmskog (May 26 2020 at 15:59):

since it lives in MathComp's repo, it's just another OPAM package definition on top of the already-released archives (and repo, for coq-extra-dev)

view this post on Zulip Cyril Cohen (Jun 06 2020 at 18:10):

Pierre-Yves Strub said:

Anyway, from master, after having fixed that and compiled order.v (unmodified), I run:

ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib ssreflect.order > check.v

I obtain a big file with a lot of checks, but it doesn't work

➜  coqc -I . -R . mathcomp check.v
File "./check.v", line 30, characters 34-39:
Error:
The term "Order.CBDistrLattice.class (id (?t : cbDistrLatticeType ?d1))"
has type "Order.CBDistrLattice.class_of (id ?t)"
while it is expected to have type "Type".

Hi @Pierre-Yves Strub I finally took the time to tale a look at this, I hadn't until I saw you mentionned kitties dying and this is unbearable...

I guess what the script does wrong is that one should close library imports transitively. I have no clue how to make the script do that (importing everything your library imports seams like a bad idea to me). So unless one finds a way to indicate to Coq the minimal context for making some file work (I guess one could turn bunches of Require Import into Require Export at the begining of mathcomp files, did someone every try that?).
So I guess the only easy remaing way is to manually provide all the required -libmanually.

In your specific case you could run ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all_ssreflect > check.v which is not as "minimal" as you might want but still takes less time than the complete all.v check.

view this post on Zulip Kazuhiko Sakaguchi (Jun 15 2020 at 17:32):

Sorry for the late reply. I had some time to fix reported issues of process handling. See #536.

view this post on Zulip Kazuhiko Sakaguchi (Jun 15 2020 at 17:41):

@Karl Palmskog hierarchy.ml has to classify the output lines of Print Canonical Projections to inheritance paths and non-trivial joins, and this part of the script is still quite ad hoc. Thus I don't want to publish it as a standalone tool as it is. I will try to make it less ad hoc tomorrow.

view this post on Zulip Kazuhiko Sakaguchi (Jun 16 2020 at 11:05):

Pierre-Yves Strub said:

Anyway, from master, after having fixed that and compiled order.v (unmodified), I run:

ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib ssreflect.order > check.v

I obtain a big file with a lot of checks, but it doesn't work

➜  coqc -I . -R . mathcomp check.v
File "./check.v", line 30, characters 34-39:
Error:
The term "Order.CBDistrLattice.class (id (?t : cbDistrLatticeType ?d1))"
has type "Order.CBDistrLattice.class_of (id ?t)"
while it is expected to have type "Type".

The actual source of this issue was that the check_join tactic uses ssrfun.id with its unqualified name. Now my PR also fixes this issue. It still fails to find the join of bDistrLatticeType and choiceType (because it does not import choice.v) but I hope the error message is now understandable. CC: @Cyril Cohen

view this post on Zulip Kazuhiko Sakaguchi (Jun 16 2020 at 11:10):

Also, I attempted to have a new make target to run this test only for all_ssreflect (without building the whole library), but there are issues with make and coq_makefile which I cannot fix right now.

view this post on Zulip Kazuhiko Sakaguchi (Jun 16 2020 at 11:22):

Emilio Jesús Gallego Arias said:

By the way Kazuhiko Sakaguchi , wouldn't it easier for hiearchy.ml to be written against Coq's ML API? That would make some of the code quite a bit more robust. [I could help but not this week, very short on cycles these days]

I think it would be nice to reimplement hierarchy.ml as a Coq plugin so that we can easily generate test cases in the middle of a .v file. In that way, we can also get more information such as types of canonical instances and may test more things such as convertibility of canonical (concrete) instances. (But I hope that hierarchy builder will subsume these functionalities.)


Last updated: Aug 11 2022 at 01:03 UTC