Stream: Hydras & Co. universe

Topic: Implicit Arguments


view this post on Zulip Pierre Castéran (Feb 24 2023 at 18:27):

In the old goedel+Ackermann library, the same constructor of the abstract syntax of FOL formula had various representations, depending of the considered module. Some redefinitions like Definition forallH := forallH LNN. resulted in some issues (complex proof scripts, difficulty to design simple notations, etc.)
In the branch Implicits, I propose a uniform abstract syntax using implicit arguments, and fix the changes in proof scripts. After some minor changes (mainly comments + indentation) , I plan to merge it into master`.

view this post on Zulip Karl Palmskog (Feb 24 2023 at 18:30):

sounds good, let us know if any help is needed with the PR/branch. I think Coq 8.17.0 is coming out soon finally, but it should work fine with CI and so on.

view this post on Zulip Pierre Castéran (Feb 24 2023 at 18:41):

Ok, next week, I will try to improve the presentation, and submit a draft PR.

view this post on Zulip Pierre Castéran (Feb 25 2023 at 17:35):

I made a draft PR. Works, except in dev (because of Equations, probably).

view this post on Zulip Karl Palmskog (Feb 25 2023 at 17:44):

hmm, one thing that comes to mind is that I believe one can locally clear implicit arguments (to avoid having a lot of @ somewhere)

view this post on Zulip Karl Palmskog (Feb 25 2023 at 17:49):

e.g., #[local] Arguments validator_state _ _ : clear implicits.

view this post on Zulip Karl Palmskog (Feb 25 2023 at 17:52):

hmm, the Equations brekage is strange, I didn't get it locally. There may be an issue with the master Docker image, but I'll wait for a day before reporting to Coq-Docker. (Image should be rebuilt overnight)

view this post on Zulip Pierre Castéran (Feb 25 2023 at 18:02):

OK, I could remove the "@" in LNT.v
I'll try to do it tomorrow (the "fol." prefix too).

view this post on Zulip Karl Palmskog (Feb 26 2023 at 09:44):

I figured out the CI issues, unfortunately the workaround I pushed in the Implicits branch makes CI take longer than usual

view this post on Zulip Pierre Castéran (Feb 26 2023 at 10:59):

I removed a lot (all ???) of "fol." prefix in front of abstract syntax constructors.

view this post on Zulip Karl Palmskog (Feb 26 2023 at 15:19):

looks reasonable to merge now to me


Last updated: Mar 28 2024 at 13:01 UTC