start of the mm0ifying process of set.mm.mm0

[Lakedaemon]

• added delimiters ( ) ~
• added operators : ->, ~, <->, /\, \/
• added definitions : wb, wo
• removed axioms : df_bi, df_or
• added theorems : df_bi, df_or

[Lakedaemon]

Hello, it would be nice if you could add a travis check of set.mm.mm0 + set.mm.mm Best regards, Olivier

[Lakedaemon]

Clippy doesn't like my pull requests :/

Next, I think that I'll try to handle "cv" And I am wondering about what to do with axiom df_clab {y1 : setvar} (ph : wff y1) (x3 : setvar) : $ (cv x3) e. { y1 | ph } <-> (wsb y1 ph x3) $;

This should probably be a notation (with a unique starting contant :/) pointing to wsb

[digama0]

Have you looked at set.mm0? This should address most of the foundational questions involved in modeling set.mm in MM0.

I don't know about hosting set.mm.mm0 directly in this repository though. set.mm changes too often - it will get out of date easily. One way to solve this is to express the edits via a patch/diff file from the set.mm.mm0 file that is generated automatically from the latest version of set.mm. That way CI can download set.mm, translate it, apply the patch file, and verify the result, and this will work as long as set.mm doesn't change significantly, especially around the axioms. Alternatively, the MM -> MM0 importer file can take a configuration file that lets you specify replacements, alignments and so on, and we only check in the configuration. (This is likely to be even more stable than using patch files, since these can get tripped up by comment changes or similar.)

[Lakedaemon]

I looked at set.mm0 and I use it as a guide but at a point, I'll get to it's end and then, I'would like to benefit from your enlighted advices (you have the power to save me a lot of time).

The set.mm.mm0 -> patched version of set.mm.mm0 IS a patch. At the moment, it looks like it is a script (written in Kotlin) that gobbles an unpatched set.mm.mm0 file and that spits out an enhanced version of set.mm.mm0

The patch is handwritten at the momen t (it helps me progress through writting more accurate parsers/proof checkers/patchers) But soon, it will automatically patch most axioims of the type axiom : newNotation <-> old stuff

[Lakedaemon]

yes, the answer about cv is in set.mm0. Nice :)

[digama0]

The set.mm.mm0 -> patched version of set.mm.mm0 IS a patch. At the moment, it looks like it is a script (written in Kotlin) that gobbles an unpatched set.mm.mm0 file and that spits out an enhanced version of set.mm.mm0

That's not what you PR'd though, I see two huge files, one of them binary and both hard to review. Please PR the kotlin program instead.

[Lakedaemon]

Indeed.

If you want the patcher And the patch, it will require more work on my side though and I am not ready to pr it yet. I see 3 ways where it can go : 1) either I release a binary that eats a Triple (mm0 file, mmu file, patch file) and that spits a proofchecked patched (mm0 file, mmu file) pair along with a patch that works on the set.mm.mm0 file that you once send me (but you can insert in in your pipeline)

2) I release the binary, the patch AND the source code for the patcher

3) you write in rust/C/mm0-C a patcher (it requires a mm0 parser, a mmu parser, a mm0-mmu proof-checker and a reasonable amount of code to write fold/unfold/handle/transform mmu proofs/dynamicParser trees and I contribute, along with others to the writing of the patch

I would rather have solution 3 as you are an expert programmer and THE expert about mm0/mmu/mm/formal logic related stuff and you have basically already written the code necessary for step 3 (mm1 should help)

but as my goals require me to write a patcher, I can do 1 and 2 also. It will juste require more time/experimentation. That is fine by me.

In the mean time, I'll keep on trying to mm0ify set.mm (because I need that). It would have been nice though to know if the official mm0/mmu proof checker validated the patch (to know if I'm going in the right way or to uncover more bugs in my code)

By the way, I found a lot of bugs in my proofchecker, after it had passed bad versions of (mm0/mmu) pair. This is a bit worrying. We should make sure that proofcheckers fail when they have bad input

Maybe, it should be in the mm0/mmu contract that proofchecker should FAIL when faced with wrong input

[Lakedaemon]

o silly me, I'll just build your stuff and proofcheck myself.. (lazy me !)

[digama0]

I would rather have solution 3 as you are an expert programmer and THE expert about mm0/mmu/mm/formal logic related stuff and you have basically already written the code necessary for step 3 (mm1 should help)

Getting this to work is not my main priority at the moment, so I would prefer to take an advisory role here; if you provide a draft of a patcher I can help with making it better. But there isn't anything for me to review in this PR as it currently exists. You don't have to release the Kotlin patcher if you don't want to, especially if it contains some closed source stuff you don't want to reveal, but it should be possible to have something equivalent to it, some combination of code and configuration that can be combined with the set.mm file to get a working MM0 file.

But keep in mind that this is an open source project. I don't want to rely on any black box executables, especially in a project like this one which is explicitly trying to bootstrap a trustworthy proof checker down to the hardware. If you can't meet these requirements, then you can just not PR it.

In the mean time, I'll keep on trying to mm0ify set.mm (because I need that). It would have been nice though to know if the official mm0/mmu proof checker validated the patch (to know if I'm going in the right way or to uncover more bugs in my code)

As you have already guessed, you should build and use the tools in this repo to do so. mm0-c only takes .mmb files, so you will first have to convert the mmu file to mmb, which you can do using mm0-rs.

# convert the MMU file to MMB
mm0-rs compile set.mm.mmu set.mm.mmb
# verify the MMB file against the MM0 spec
mm0-c set.mm.mm0 < set.mm.mmb

You need rust to compile mm0-rs and gcc to compile mm0-c; there are readmes in the respective directories which explain the build process.

[Lakedaemon]

Ok. What about if I contribute with :

• a mm0 parser
• a mmu parser
• a mm0/mmu proof-checker
• a mm0/mmu patcher (no promise about conservation of comments in mm0 files) in Kotlin, with a very permissive mit/apache2/bsd license (If I publish it, you do what you want with the code) ?

If it is ok, what could the package name scheme be ? (I would rather avoid org.lakedaemon.mmu or com.mephistolus.mmu for a public open source release)

[digama0]

An MIT or BSD license is fine by me, although you will have to keep a separate license file because most of this repo is "CC0 / public domain unless otherwise specified". Most of the projects in this repo are named after the language they are written in, and I would just use that for the package name, like org.mm0-kt or something.

[Lakedaemon]

No, I'll use your "CC0 / public domain unless otherwise specified" license. Less worry...and everybody can use the code. I like it this way. I give, no strings attached.

But, pretty please, keep on advising me, please. You give good advice and I need it.

I'll slowly publish some stuff usefull to the mm0 project, then...

[Lakedaemon]

I'm closing this pr. I am reworking my code so as to contribute the promised mm0/mu parsers mm0-mmu proofChecker mm0/mmu patcher as well as a patch (work in progress).

I hope you'll be able to integrate that in your pipeline (because a set.mm.mm0/set.mm.mmu pair exported from set.mm will be needed)

The patcher will probably take a zip file with set.mm.mm0 and set.mm.mmu and spit out another zip-file with the patched versions... so as to be efficient space-wise

This helps me clean my code and I'll have a sane/optimized foundation for my further works which is a good thing