generate.sh -> Makefile

[liyishuai]

No description provided.

[Zimmi48]

If you do this change, you need to fix the README. Can you briefly summarize the motivation?

[palmskog]

I'm not sure I understand how this improves the (already problematic) situation of integrating a script like generate.sh into an existing project. For example, one needs to control the names of some target files, such as for coq.opam -> coq-myproject.opam, and a Makefile effectively prevents this.

Also, let's say the templates directory lives in some completely different location from the Coq project. How can one then call the Makefile here from the Coq makefile and get paths to work out?

[liyishuai]

I see. I should change the configuration to assume templates in a subdirectory.

[palmskog]

My general argument is basically that I don't think a Makefile is flexible enough to accommodate the many workflows which one could incorporate the templates into. In particular, I think we need some kind of solution that works both when templates is in a subdirectory (of the current Coq project) and when it lives somewhere completely different. The parametrization (pattern-matching, really) in Makefiles (%.mustache and so on) is also lacking in flexibility. Finally, not many people will want to use files like the index.md template by default (it's an "extra" when there is a website).

The current generate.sh script is not great at all, but I think there should at least be some improvement on the above issues for a replacement.

[liyishuai]

Changes:

• Moved example to subfolder
• Specific rules for .opam files
• Replaced target index.md with index.html

[Zimmi48]

If I understood correctly, this PR has been made obsolete by #26 and all that remains to do is to address #20 and #24.