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.
In MathComp, make test-suite
lets you run hierarchy.ml
properly.
But it requires all/all.vo
and thus has to compiles MathComp entirely.
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]
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.
Ok, I adapted the Makefile
rule to my needs -- because compiling mathcomp each time if want to check a file won't do it.
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 ()
.
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".
(Also, the script should check the exit status of coqtop
. Each time a syscall return code is ignored, a kitty dies)
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
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
)
Pierre-Yves Strub said:
Anyway, from
master
, after having fixed that and compiledorder.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 -lib
manually.
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.
Sorry for the late reply. I had some time to fix reported issues of process handling. See #536.
@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.
Pierre-Yves Strub said:
Anyway, from
master
, after having fixed that and compiledorder.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
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.
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: Oct 13 2024 at 01:02 UTC