Refactor coq-waterproof into a Coq plugin

impermeable / coq-waterproof

GNU Lesser General Public License v3.0

29 stars 9 forks source link

Refactor coq-waterproof into a Coq plugin #14

Closed RatCornu closed 1 year ago

RatCornu commented 1 year ago

refactor: coq-waterproof into a Coq plugin written in OCaml and in Ltac2
feat(automation): creation of wauto and weauto with backtracking support
feat(CI): add build and documentation CI to the repository

jim-portegies commented 1 year ago

Could it be that the Help tactic is not ported?

jim-portegies commented 1 year ago

While running "make install" manually, the test files are not installed but skipped. In principle, this should be fine, but the message is "SKIP tests/... since it has no logical path". Perhaps it is better if this does not show up?

RatCornu commented 1 year ago

Could it be that the Help tactic is not ported?

Indeed I forgot to port it : it is now done

RatCornu commented 1 year ago

While running "make install" manually, the test files are not installed but skipped. In principle, this should be fine, but the message is "SKIP tests/... since it has no logical path". Perhaps it is better if this does not show up?

I can search a workaround to remove those messages, but I think it is due to Coq's makefile implementation that does not install compiled files that are not necessary to the plugin : those ones are indicated with a -R or a -I option in the _CoqMakefile.in file.