Closed 1DGW closed 1 month ago
From the upstream repository I see you don't use coq_makefile. It would generate an install
target for your package.
You are free not to use coq_makefile, but you have to provide it, indeed CI fails saying that there is no make install
target.
For your convenience, here a link to the doc of coq_makefile https://coq.inria.fr/doc/V8.19.0/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile-details
@1DGW @gares I did a PR with the standard boilerplate, to me this would be a requisite for getting a package merged: https://github.com/1DGW/formalization-of-Morse-Kelley-axiomatic-set-theory/pull/1
We would like to contribute the formalization of the Morse-Kelley axiomatic set theory.