including extracts from an old contrib about hydra-battles HOT 9 CLOSED

from hydra-battles.

Sounds good to me.

from hydra-battles.

@Casteran I agree in general, but I think it's fine to change statements and module names conservatively as long as pull requests are submitted to the goedel repo in reasonable time (so that each Coq stable version has a working release of the incompleteness theorem).

from hydra-battles.

Yes, I agree that it would make sense to copy just these three files as it would cut the dependency on pocklington.

from hydra-battles.

@Zimmi48 @palmskog
Te branch with-ackermann has been made quickly (by naively copying files). It iits structure is OK, there should exist
a way to move these files from a project to another ?

from hydra-battles.

Yes, there are tricks to move files while keeping the git history thanks to git subtree.

from hydra-battles.

It's fine by me to move the Ackermann library to hydra-battles for easier development, but at the same time I believe:

• we should leave the rest of Gödel's incompleteness theorem in the goedel repo, not least for visibility reasons - this is basically an important Coq formalization milestone that should be easy to locate
• we should make sure the goedel repo and package can build properly with hydra-battles as a dependency
• we should preserve the history of the Ackermann library via git subtree

How does that sound to you @Zimmi48?

from hydra-battles.

@palmskog @Zimmi48

Perhaps the (present and future) maintainers of hydra-battles should follow the following politics

• add doc, bullets, etc, to the historical modules of Ackermann
• do not modify statements, implicit arguments, names of these modules,
• useful changes may be done in new modules, not required by Goedel

We may write such a warning in the README

from hydra-battles.

I think we can close this issue now, please reopen if it becomes relevant again.

from hydra-battles.