How do I contribute to mmil.html?

[jkingdon]

Hey, before I put this in pull request form, just wanted to check whether this is the right place.

I came up with an expansion to mmil.html (basically, a start on an axioms section for intuitionistic propositional logic) which can be found here; https://github.com/digama0/set.mm/pull/1

I'm not quite sure what version of mmil.html I should be starting from or how I should be formatting my submission (or even whether that file is generated from something else, for that matter). I'd be glad to do some of that if I can usefully do so,, or alternatively, just take a look at the diff at the above URL if that is sufficient.

As for my larger interests, I wrote the intuitionistic proofs and text over at http://wikiproofs.org/w/index.php?title=Category:Subsystems_of_classical_logic and would love to bring that to a larger community with more mature tools. I'd also like to look into type theory of various kinds, although that's a bigger topic (partly because I'm still learning type theory, partly because how to fit it into metamath is, I guess, less obvious than intuitionistic propositional/predicate logic).

Thanks,

Jim

[nmegill]

As far as I know, mmil.html is not under revision control (Mario can correct me if I am wrong) because updates have been very rare so far, and the most recent version is the one on http://us2.metamath.org:88 . For these kinds of cases you would just email me the file or point me to it, and I will update it for the next site build. I'll wait for Mario's approval since he originated the file, then I will update it for you.

Norm

On 11/12/17 12:26 PM, Jim Kingdon wrote:

Hey, before I put this in pull request form, just wanted to check whether this is the right place.

I came up with an expansion to mmil.html (basically, a start on an axioms section for intuitionistic propositional logic) which can be found here; digama0/set.mm#1 https://github.com/digama0/set.mm/pull/1

I'm not quite sure what version of mmil.html I should be starting from or how I should be formatting my submission (or even whether that file is generated from something else, for that matter). I'd be glad to do some of that if I can usefully do so,, or alternatively, just take a look at the diff at the above URL if that is sufficient.

As for my larger interests, I wrote the intuitionistic proofs and text over at http://wikiproofs.org/w/index.php?title=Category:Subsystems_of_classical_logic and would love to bring that to a larger community with more mature tools. I'd also like to look into type theory of various kinds, although that's a bigger topic (partly because I'm still learning type theory, partly because how to fit it into metamath is, I guess, less obvious than intuitionistic propositional/predicate logic).

Thanks,

Jim

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/metamath/set.mm/issues/154, or mute the thread https://github.com/notifications/unsubscribe-auth/AMKLqHID-r4zxH7zarpvPZR_hVKGGAcCks5s1yo4gaJpZM4Qa9zU.

[david-a-wheeler]

On November 12, 2017 3:24:35 PM EST, nmegill notifications@github.com wrote:

As far as I know, mmil.html is not under revision control (Mario can correct me if I am wrong) because updates have been very rare so far, and the most recent version is the one on http://us2.metamath.org:88 .

It would be best if it was under Version Control, and separately from set.mm since they are independent. --- David A.Wheeler

[digama0]

I'm 100% okay with updates to the intuitionistic logic stuff, and the HTML was a stub to begin with, so I'm happy to see new content there.

Maybe this is an indication that we should get more of the web site material under version control, either here or in a separate repository. Besides making contributions easier, this would allow for more Travis checking of the other mm files. But it's up to you.

[jkingdon]

Version control would be great (for one thing, I'm hoping to make updates less rare, for another thing it would be a good way for me to solicit comments). If you'd like me to email a file, I can do that, but I'd want to prepare one based on http://us2.metamath.org:88/ileuni/mmil.html (I thought I was doing that before, but it looks like I accidentally got some differences by saving in a web browser, rather than a mechanism like curl which preserves the file as it was downloaded).

[david-a-wheeler]

Let me modify my earlier comment... If it would make sense to have them in a single repository, that would also be fine. I just think that we ought to have the intuitionistic stuff under Version Control somewhere.

[nmegill]

On 11/12/17 6:29 PM, Jim Kingdon wrote:

Version control would be great (for one thing, I'm hoping to make updates less rare, for another thing it would be a good way for me to solicit comments). If you'd like me to email a file, I can do that, but I'd want to prepare one based on http://us2.metamath.org:88/ileuni/mmil.html (I thought I was doing that

Please do start with this one.

There is an w3c validator link at the bottom of the page. Please make sure that it passes.

Email it to me or point me to it, and I'll update the site and add it to the set.mm develop branch. From that normal pull requests can be made.

So far, all user-created files have unique names regardless of directory, so we won't have any naming conflicts. At some point we can think about a directory structure e.g. mirror the site, but that can be postponed. (Actually I will be doing some directory reorganization independently of this anyway. I want to make the master directory uni instead of gif to match our recent switch to *uni as the default.)

Note that any user-created html file associated with a database directory (like mpeuni or ileuni) must start with "mm" to avoid conflict with theorem web pages. The "verify markup" command in metamath.exe checks that no statement label begins with "mm".

Norm

before, but it looks like I accidentally got some differences by saving in a web browser, rather than a mechanism like curl which preserves the file as it was downloaded).

[nmegill]

Actually, I just added mmil.html to the develop branch. So you can do a pull request for your version instead of emailing me.

Norm

[jkingdon]

Thanks, @nmegill . I'll make a pull request soon (probably tonight or tomorrow).

[jkingdon]

I've submitted a pull request at https://github.com/metamath/set.mm/pull/155