search

barry-jay-personal / tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus
MIT License
51 stars 4 forks source link

remove generated files, use simple delegating makefile and coq_makefile #1

Closed palmskog closed 4 years ago

palmskog commented 4 years ago

I saw that your release tarball, and thus the repository, contained binary (compiled, .vo) files. These files take a lot of space and are very tightly coupled to a specific version of Coq and the platform that Coq was built on (e.g., x86-64 on Windows). Hence, it's a bad idea to keep these files in version control on GitHub.

In this pull request, I remove these generated files and introduce a very general Makefile that works both for Coq version 8.12 and (very likely) future versions. The previous makefile is, like the compiled files, tied to a specific version of Coq. As a side effect, this makes the project checkable not only with Coq 8.12, but also 8.11. The project is still built and installed with the exact same commands, e.g., make install.

barry-jay-personal commented 4 years ago

Thanks, palmskog. My only concern was that it takes some time (20-30 minutes) to make everything, but I am happy to be guided on good practice.

palmskog commented 4 years ago

Unfortunately, having .vo files will generally not save time, unless one is using a container image with Coq (e.g., Docker).

However, if all a user is interested in is playing around with your code/theory, they could use the following command to build the project, which avoids checking any proof:

make vos

On my machine, this just takes a few seconds.

barry-jay-personal commented 4 years ago

Thanks for this, Karl. Do let me know if you have any questions. Barry

Sent from my iPhone

On 1 Oct 2020, at 6:30 pm, Karl Palmskog notifications@github.com wrote:

 Unfortunately, having .vo files will generally not save time, unless one is using a container image with Coq (e.g., Docker).

However, if all a user is interested in is playing around with your code/theory, they could use the following command to build the project, which avoids checking any proof:

make vos On my machine, this just takes a few seconds.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub, or unsubscribe.