search

SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

Zariski Topology #23

Closed dan323 closed 1 year ago

dan323 commented 1 year ago

Definitions and results on ideals, until defining the Zariski topology and computing their interior and closure operators

dan323 commented 1 year ago

This merge request deals with #24

dan323 commented 1 year ago

@SKolodynski I updated the branch to have no conflicts. You may start looking at it and comment on the files.

SKolodynski commented 1 year ago

Just to clarify how the process on my side looks like: For the changes that apply to a theory not presented at the IsarMathLib site (i.e. the ones not listed in the theories.conf file) I do very little. I just read them so that I am able to write a summary on my blog at the next release, sometimes I correct an obvious typo. I know your contributions are excellent and there is no need to scrutinize how things are done. Changes to the files presented at isarmathlib.org typically require more work as I need to get them to the state where they pass through the isar2html2.0 tool that generates the site. If there are errors I usually modify the proof. Sometimes I extend the parser, but I am reluctant to do that because I try to keep the syntax presented at the site as simple as possible. Of course I am open to discussions about new syntactic elements but the rule is that the their usefulness must well justify additional syntactic complexity (as was the case for sublocale command for example). I still don't know the proper git incantations to make this process as smooth as possible. In the near future I am planning to add another check that would run isar2html so that I know when I can merge the changes from the GitHub interface without having to go through checking out and modifying the changes locally.

In case of this PR I see there are no changes to the files listed at theories.conf file) so I would like to just merge it now. Would you like me to wait with this for some reason?

dan323 commented 1 year ago

This is one of the points I tried to get across some time ago. We need to run the parser in the github workflow, so I know when I am overstepping. I added your verification to PRs, because you did it only on push; but I do not think it is parsing.

dan323 commented 1 year ago

I rebased to apply the style-check workflow

dan323 commented 1 year ago

@SKolodynski do not merge this one yet. Merge the one about the parsable file. I will update this branch after that one is merged.

dan323 commented 1 year ago

@SKolodynski I rebased again. You may merge if everything is correct