Stream: Teaching [with] Coq

Topic: French high school geometry in Coq

Karl Palmskog (Nov 22 2023 at 10:32):

I'd just like to flag up that this project is in need of more active maintenance (e.g., a co-maintainer): https://github.com/coq-community/HighSchoolGeometry

It formalizes geometry at the level of French high school. It has a companion paper in French, and many Coq constant names are in French. Would be nice if there was some larger "Coq math library for teaching" project it could be integrated into (and Coq-community would be happy to host such a project)

Julio Di Egidio (Nov 22 2023 at 15:07):

I'd be glad to give some time to community projects, and that one sounds maybe not above my head, plus I can speak/write French, though it's quite rusty. But, if I can ask you: 1) I am not sure about the "scope" of these projects, would I even be eligible? and, 2) I have looked at that project on GitHub and see no issues and no todo's, could you give an idea of the kind of work involved (eventually, for the competences needed and the amount of effort one should anticipate)? Thanks.

Karl Palmskog (Nov 23 2023 at 07:58):

@Julio Di Egidio for this project, the effort could have the following range, depending on your preference:

• minimal: keeping the project working with the latest released version of Coq, keeping up-to-date with CI configuration best practices, performing minor changes to make maintenance more efficient, doing GitHub tags/releases now and then
• ambitious: reorganizing/refactoring code to make it simpler or more understandable, porting to use another library besides Coq Stdlib

For the "minimal" version, I'd say about an hour per month could suffice. A more ambitious approach could take an hour per week or more. Maintainers can decide what they will put in.

Since there is already a nominal maintainer for the High School Geometry project, any radical changes to code are best to discuss first with that maintainer. But basic maintenance doesn't really need much communication/coordination.

Karl Palmskog (Nov 23 2023 at 09:06):

here is a quick writeup of what I consider Coq project maintainers can/should do: https://github.com/coq-community/manifesto/issues/3#issuecomment-1824028792

Julio Di Egidio (Nov 23 2023 at 12:59):

Thanks very much Karl: in terms of availability, I could even go for the more "ambitious" involvement, the problem is so far I have not even tried once to compile Coq from source, nor I am an expert in that side of things, so it could take me some time to be sufficiently autonomous: IOW, I might very well need some guidance/help to get started. -- That said, if you or the maintainer think that could be acceptable, please feel free to get in touch with me directly (here via PM, or maybe on GitHub, or even my email if you have it).

Karl Palmskog (Nov 23 2023 at 13:01):

the usual process is simply that we invite a new maintainer to be a member of the Coq-community organization on GitHub, and that they then get administrator privileges for the repository they maintain.

Karl Palmskog (Nov 23 2023 at 13:02):

the current nominal maintainer of the HighSchoolGeometry repo is @Laurent Théry, I don't think he minds having a co-maintainer, but I ping here as courtesy

Julio Di Egidio (Nov 23 2023 at 13:11):

OK, I think it will take me several days to set my things up (I need a virtual machine, thinking Ubuntu, and I need to try and compile the whole thing: and I will certainly have some issues I would ask for help here on Zulip), but I can confirm my availability and willingness to at least try.

Karl Palmskog (Nov 23 2023 at 13:14):

for this project, we don't really have much of a rush in development. I recently did some small updates so it should work with recent Coq.

Karl Palmskog (Nov 24 2023 at 08:46):

to get started, I recommend creating a new branch in the repo and then a pull request against master based on that branch with a small change such as that described here: https://github.com/coq-community/HighSchoolGeometry/issues/10

CI will check that the change works with several Coq versions.

Julio Di Egidio (Nov 24 2023 at 12:48):

Hi Karl, I am still in the process of installing Ubuntu, I just cannot use directly my PC.

Then I will try and follow your indications: of course I might botch some conventions, but the changes here look minimal so no problem if I have to redo/repack the whole thing up to the PR.

Anyway, I will keep you posted (here): most probably I will have some questions.

Julio Di Egidio (Nov 25 2023 at 14:19):

[I have few questions about how to proceed here: should I rather ask these questions on the Issues page?]

I have made the requested changes and it all compiles fine. Few questions to proceed:

1) There are exactly these three files that reference the stdlib:

• Field_affine.v
• Rutile.v
• vecteur.v

and the Requires at the moment are in the form of a plain Require Export XYZ.

I have already verified that these all work with From Coq Require Export XYZ.

So, should I change those too while I am at it?

2) I am going to use:

• "Ensure the project builds with -Q option" as the branch name;
• idem for the commit message.

Would that be OK? -- If you confirm, I am going to finish, then push, then I'll think about the PR...

Sorry for so many question, first-timer. Thank you.

cc: @Karl Palmskog

Karl Palmskog (Nov 25 2023 at 14:20):

for any files referencing Stdlib, best practice is to replace with From Coq Require Export XYZ when it says Require Export XYZ. This is because Stdlib is expected to become its own standalone library in the future.

Karl Palmskog (Nov 25 2023 at 14:21):

I recommend using a simple short branch name such as q-compilation. Commit messages can be longer and more descriptive.

Julio Di Egidio (Nov 25 2023 at 14:22):

OK, perfect, will proceed accordingly. Thank you.

Julio Di Egidio (Nov 25 2023 at 18:55):

@Karl Palmskog Changes just pushed. I will look tomorrow into creating the PR...

Karl Palmskog (Nov 25 2023 at 18:59):

but I think you get the URL to create the PR from the push message, right? It's basically one click to create a PR.

Julio Di Egidio (Nov 25 2023 at 19:01):

I have pushed from the command line, and I closed it meanwhile: but I don't remember any message.

I was thinking about doing the PR directly on GitHub...

Karl Palmskog (Nov 25 2023 at 19:02):

You can just go to the following URL and click the button to open the PR: https://github.com/coq-community/HighSchoolGeometry/pull/new/q-compilation

This way, CI will run for the changes

Julio Di Egidio (Nov 25 2023 at 19:02):

OK, doing it...

Julio Di Egidio (Nov 25 2023 at 19:03):

It's not yet attached to the issue, right? Should I proceed anyway?

Karl Palmskog (Nov 25 2023 at 19:03):

typically, after pushing a GitHub branch, one gets a command-line message like this:

remote: Create a pull request for 'my-branch' on GitHub by visiting:
remote:      https://github.com/example/fork/pull/new/my-branch

Karl Palmskog (Nov 25 2023 at 19:04):

you can add a string Closes #10 in the comment to the PR, and the issue will be linked

Julio Di Egidio (Nov 25 2023 at 19:05):

OK, done: it's working now...

Julio Di Egidio (Nov 25 2023 at 19:10):

It's done. Should I push merge? :) In fact, I am not terribly familiar with what happens past that point: please feel free to take over.

There is also deleting the branch: would you like me to do that as well (though tomorrow at this point)?

Karl Palmskog (Nov 25 2023 at 19:12):

since it passed CI, fine by me to merge. We usually delete branches after they have been merged into master

Karl Palmskog (Nov 25 2023 at 19:12):

there will be a button to delete the branch in the GitHub pull request page after the merge button has been pushed

Julio Di Egidio (Nov 25 2023 at 19:13):

OK great, and thanks for your guidance: I will do the merge now, then I will have to close for the day: will take it up tomorrow...

Julio Di Egidio (Nov 25 2023 at 19:14):

I am seeing it...

Julio Di Egidio (Nov 25 2023 at 19:14):

OK, deleted also the branch: all done!

Karl Palmskog (Nov 26 2023 at 10:08):

followup issue: https://github.com/coq-community/HighSchoolGeometry/issues/12

Julio Di Egidio (Nov 26 2023 at 12:08):

OK, I should be able to do it this afternoon. I will search for "Qed" or "Defined" to catch them all...

Karl Palmskog (Nov 26 2023 at 12:14):

one possible alternative way is to search for the "theorem" keywords: Theorem, Lemma, Corollary, Example (https://coq.inria.fr/doc/V8.18.0/refman/language/core/definitions.html#grammar-token-thm_token). Then you scan to the end of that sentence (indicated by .) and insert a newline and Proof. by itself on a separate line.

Julio Di Egidio (Nov 26 2023 at 12:17):

In Definitions as well, that's why Qed and Defined seem the ones that get them all...

Karl Palmskog (Nov 26 2023 at 12:19):

it's not as obvious to use Proof. in Definition/Fixpoint, because that will hide the body of the definition with some documentation generators

Karl Palmskog (Nov 26 2023 at 12:20):

I have a longstanding Coq change idea I hope to get in to Coq 8.20: adding Body. as a synonym to Proof.. This will allow documentation generators to distinguish "proof scripts" from "function bodies"

Julio Di Egidio (Nov 26 2023 at 12:24):

I should think about it: one "strange" thing about Coq is that most of these words are synonyms, which on a side makes perfect sense due Curry-Howard, but the proliferation of keywords/vernacular I find potentially more confusing than anything else (and then one has to establish internal conventions and so on)... it's certainly not a trivial balance to strike.

Karl Palmskog (Nov 26 2023 at 12:27):

well, you have to distinguish between the surface language (vernacular) and the term language. A lot of things in the surface language don't have any effect on the terms, but are rather where maintainers can enforce different conventions for maintainability/readability

Karl Palmskog (Nov 26 2023 at 12:29):

Andrej Bauer has this nice breakdown:
anatomy.png

Julio Di Egidio (Nov 26 2023 at 12:30):

A lot of things in the surface language don't have any effect on the terms

That is the opposite of what one usually strives for in a programming language, or even in a domain specific one: for example a principle is "one and only one way to write anything"...

In Andrej's terms, we lose "exact"...

Karl Palmskog (Nov 26 2023 at 12:30):

for historical reasons Definition is not a full synonym of Theorem/Lemma, but in the future, the meaning will likely be exactly the same

Karl Palmskog (Nov 26 2023 at 12:32):

but one consequence of Curry-Howard is that Prop being interpreted as propositions in the usual logic sense is just a convention, and people can just as well choose between Set/Type/Prop depending on their requirements/needs for impredicativity, extraction, universe handling, etc.

Karl Palmskog (Nov 26 2023 at 12:33):

I don't think we loose "exactness" by having Theorem and Definition as synonyms. It's a help for the reader of the code on what the writer intended, with the understanding that both writer and reader knows that the term is the same regardless

Karl Palmskog (Nov 26 2023 at 12:36):

one analogy is that many syntactically different Java programs will have the same meaning due to them being mapped to the same JVM bytecode by the compiler. I don't think Java becomes inexact because of this

Julio Di Egidio (Nov 26 2023 at 12:38):

Even in Java you do not have 5 keywords that are all synonym to "class" for example...

Julio Di Egidio (Nov 26 2023 at 12:39):

The problem not only is with the reading/learning the language, the problem is also maintenance and doing e.g. searches across files...

Karl Palmskog (Nov 26 2023 at 12:40):

but search in Coq often needs to be done at term level anyway. For example, Z.add_comm doesn't exist in the source, it's generated by functors/modules

Julio Di Egidio (Nov 26 2023 at 12:40):

Searches across files, Karl...

Karl Palmskog (Nov 26 2023 at 12:41):

sure, but I'm saying that "files" is usually not even the right abstraction level to perform search

Julio Di Egidio (Nov 26 2023 at 12:42):

Code maintenance proper is a dirty business having to do with text files. Anyway, as I said, just my immediate thoughts.

Paolo Giarrusso (Nov 26 2023 at 13:15):

Search in Coq needs to be done on ASTs but it can't today.

Paolo Giarrusso (Nov 26 2023 at 13:16):

I personally agree with Julio, OTOH math prose has the same "feature" and nobody really objects there.

Karl Palmskog (Nov 26 2023 at 13:18):

I'd say search can't be conveniently done on ASTs today. There are various tools that can extract/juggle ASTs, but none of them are integrated into regular Coq workflows/tools

Karl Palmskog (Nov 26 2023 at 13:20):

right, arguably many of the most important results in applied math are viewed by pure mathematicians as "just lemmas"

Paolo Giarrusso (Nov 26 2023 at 13:22):

I suspect the lemma/theorem distinction belongs purely in comments... Agda has no such keyword and I don't think I've ever seen Agda users wish for it?

Paolo Giarrusso (Nov 26 2023 at 13:22):

But for now, the subtle differences between "synonyms" are a much bigger annoyance.

Karl Palmskog (Nov 26 2023 at 13:24):

but Agda doesn't even have proof scripts... do they even call their term bodies "proofs"?

Karl Palmskog (Nov 26 2023 at 13:27):

Quanta notwithstanding, Coq has been meant for both math "proofs" and computer science "verification" since the beginning

Paolo Giarrusso (Nov 26 2023 at 15:05):

People definitely write proofs in Agda; the syntax is inspired more by Haskell than by OCaml.

Karl Palmskog (Nov 26 2023 at 15:06):

but there is no Prop sort, right? So it's more "types in lieu of propositions" than "propositions as types"

Paolo Giarrusso (Nov 26 2023 at 15:08):

Some would say that "propositions as types" is closer to Agda than Coq — conjunctions are literally products, etc.

Paolo Giarrusso (Nov 26 2023 at 15:09):

If you care about propositions, ask the HoTT and Cubical Agda folks, but that doesn't really matter for syntactic PL proofs

Paolo Giarrusso (Nov 26 2023 at 15:09):

Say, for the POPLmark challenge.

Julio Di Egidio (Nov 26 2023 at 16:25):

Code maintenance proper is a dirty business having to do with text files

I have easily fixed the one Lemma with an occurrence of "Defined", as for "Qed" I get 1153 occurrences in 69 file. And I suppose it is going right now to be easier for me to just go through the files one by one, it is not so many files anyway... (I am in fact in the process of doing it.)

But, in a more general perspective, would there be a way here to write say a shell script that parses the files and inserts "Proof.\n" where needed (by searching for "Qed." then scanning back to any of "Theorem" or "Lemma", etc.)?

Karl Palmskog (Nov 26 2023 at 17:01):

I'd recommend using something like sed or awk to do the replacement. It will likely be hard to get all of them (all occurrences of missing Proof.) working at once. If you write a script, we have no obvious repo to put it in, but you could make it a GitHub Gist and link it here: https://github.com/coq-community/manifesto/issues/3

Julio Di Egidio (Nov 26 2023 at 17:11):

Indeed in this case even a regex might do the trick, assuming there is nothing but basic syntax in these file... and that's indeed the other side of the coin, making sure it's working and catching all it needs. On 69 files I am going to be faster doing it by hand anyway... But for the general case I think leveraging serapi or something similar would be the only way to reliably parse .v files, right?

Karl Palmskog (Nov 26 2023 at 17:55):

yes, accessing Coq's parser via something like SerAPI is the only reliable way to find beginning of proof mode

Julio Di Egidio (Nov 26 2023 at 18:03):

OK, thanks, makes sense.

Meanwhile I am going through the changes and I am finding myself uniformizing end of files adding a new line where it's missing (some files have it, some don't): is that OK or you'd rather prefer that I do not touch that?

Karl Palmskog (Nov 26 2023 at 18:05):

the general convention is that files end with newline, many editors enforce this. Fine by me to do those changes at the same time as other changes

Julio Di Egidio (Nov 26 2023 at 20:38):

@Karl Palmskog I have just created the PR, it's now being checked.

Sorry, I have botched the Issue reference, should have been #12, I wrote #11: I hope that can be fixed later, I don't want to risk to interrupt what it's doing...

Julio Di Egidio (Nov 26 2023 at 20:42):

OK, all verified successfully and fixed the link to the issue (GitHub seems to have picked it up fine).

I will be waiting for your confirmation before merging...

Karl Palmskog (Nov 26 2023 at 21:09):

@Julio Di Egidio I think there will be a lot of overhead if you ping me here. I think you can use GitHub's "request review" feature for a new PR if my review is important. Clearly, this change is really "either it works or it doesn't" so I don't think my approval is needed for a merge here

Julio Di Egidio (Nov 26 2023 at 21:10):

OK, thank you, I wasn't sure how to go about that: I will proceed with merging this one then.

Karl Palmskog (Nov 26 2023 at 21:11):

this is basically all there is to maintenance of most Coq projects: we do PRs with well-scoped changes, mostly to ensure CI passes before merge to master/main

Karl Palmskog (Nov 26 2023 at 21:14):

I will do some more small suggestions as issues in the next few days, but I think you've got the hang of most basics now, so feel free to work on them whenever convenient

Julio Di Egidio (Nov 26 2023 at 21:16):

Yes, indeed it's all pretty smooth. Looking forward to my next assignment(s). :)

For now, have a good rest of the week-end.

Last updated: Oct 13 2024 at 01:02 UTC