search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

Alectryon fails to handle valid Coq files because it does not pass `--topfile` #28

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

Consider the following:

$ cat foo.v
Axiom test : Set.
Check foo.test.
$ ../alectryon/alectryon.py foo.v
!! Coq raised an exception:
       The reference foo.test was not found in the current environment.
   Results past this point may be unreliable.
   The offending chunk is delimited by >>>.<<< below:
       Axiom test : Set.
       Check >>>foo.test<<<.

This causes the Alectryon to not be able to handle HoTT, for example, c.f. https://github.com/HoTT/HoTT/runs/2353786837?check_suite_focus=true#step:5:2158

cpitclaudel commented 3 years ago

Yep, I wanted to make it the default soon (https://github.com/cpitclaudel/alectryon/issues/7); do you want to make a patch? IIRC there's even commented-out code for that

cpitclaudel commented 3 years ago

Done in https://github.com/cpitclaudel/alectryon/commit/241151a8cb71d8d3c8a31bf1012cc2ed7b6ab904

The real horror show starts at https://github.com/cpitclaudel/alectryon/commit/241151a8cb71d8d3c8a31bf1012cc2ed7b6ab904#diff-ecdc6ba2577d950e32db3735d85a4a141292797346bbb06cf1197fee0bcddc06R281