search

coq-community / hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
https://coq-community.org/hydra-battles/doc/hydras.pdf
MIT License
68 stars 12 forks source link

Apply renaming #96

Closed Casteran closed 3 years ago

Casteran commented 3 years ago

Failed attempt to add Set Apply With Renaming in the three problematic files.

Zimmi48 commented 3 years ago

The failure is now in three other files: theories/ordinals/Ackermann/folProp.v, theories/ordinals/Hydra/Hydra_Examples.v and theories/ordinals/Hydra/Hydra_Termination.v. This does seem to indicate that setting the option in the files where you've done that was a correct fix but that there are just more files that are affected by this change.

Casteran commented 3 years ago

Ok! I will try this afternoon

Envoyé de mon iPhone

Le 12 oct. 2021 à 09:05, Théo Zimmermann @.***> a écrit :

The failure is now in three other files: theories/ordinals/Ackermann/folProp.v, theories/ordinals/Hydra/Hydra_Examples.v and theories/ordinals/Hydra/Hydra_Termination.v. This does seem to indicate that setting the option in the files where you've done that was a correct fix but that there are just more files that are affected by this change.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

Casteran commented 3 years ago

Ok, it looks to be a convergent process. I will iterate it after lunch 😄

Zimmi48 commented 3 years ago

And now it detected this problem in three additional files: theories/ordinals/Ackermann/code.v, theories/ordinals/Ackermann/model.v and theories/ordinals/Ackermann/subProp.v :disappointed:

Casteran commented 3 years ago

It looks like it signals the three first errors, then stops. Since nat is well-founded (proved in Coq) I hope to solve it !

Envoyé de mon iPhone

Le 12 oct. 2021 à 11:59, Théo Zimmermann @.***> a écrit :

And now it detected this problem in three additional files: theories/ordinals/Ackermann/code.v, theories/ordinals/Ackermann/model.v and theories/ordinals/Ackermann/subProp.v 😞

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

Casteran commented 3 years ago

The error changed ! Looks like to be related with coq-equations.

Zimmi48 commented 3 years ago

Yes, that's because a PR with overlays has just been merged in the Coq repository. The Docker-Coq image was probably not built yet when CI run. But this is done now, so restarting the job should solve this issue. I'll do that.

Zimmi48 commented 3 years ago

Now failing in theories/ordinals/Ackermann/codeSubFormula.v and theories/ordinals/Ackermann/subAll.v.

Zimmi48 commented 3 years ago

And now: theories/ordinals/Ackermann/folLogic3.v

Casteran commented 3 years ago

I just pushed a commit with the flag on every file of Ackermann

Envoyé de mon iPhone

Le 12 oct. 2021 à 16:19, Théo Zimmermann @.***> a écrit :

And now: theories/ordinals/Ackermann/folLogic3.v

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

Zimmi48 commented 3 years ago

Looks like it worked :tada:

Zimmi48 commented 3 years ago

The deletion of theories/ordinals/Ackermann/primRecbuggy.v is intended?

Casteran commented 3 years ago

Yes, it was outside _CoqProject.

Envoyé de mon iPhone

Le 12 oct. 2021 à 16:48, Théo Zimmermann @.***> a écrit :

The deletion of theories/ordinals/Ackermann/primRecbuggy.v is intended?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

Casteran commented 3 years ago

@Zimmi48 I let you deal with PR #95 ?

Zimmi48 commented 3 years ago

Sure!