Re: [Metamath] Mnemonic of Fr

My guess was "(well-)founded relation" as well, but Takeuti and Zaring are saying "foundational relation" in description of the 6.21 definition for Fr. If the Fr syntax is riffing off T anyway, I think it'd be an epsilon improvement to mention where the mnemonic comes from in the comment.

Re: [Metamath] Question abouot indistopon

> It functions much like A e. _V would. A proof using this theorem can always > plug in _V for V but it also could plug in On, RR, or whatever is convenient. > Perhaps looking at makes it clear. Okay, elements of ZF classes are always sets, so A e. V

Re: [Metamath] Metamath Website not loading

Jim Kingdon wrote: > > > On September 9, 2023 3:29:19 PM PDT, heiphohmia via Metamath > wrote: > > . FYI, the README > >in metamath-website-scripts still mentions contacting Norm  > > If this is the mention I am thinking of, I'm way ahead of you: > htt

Re: [Metamath] Metamath Website not loading

> Secondly, you have done a great job of publishing the various scripts so > that we can see what is going on (and at least in theory, help too) at > https://github.com/metamath/metamath-website-seed and > https://github.com/metamath/metamath-website-scripts (one can find, for > example, a

Re: [Metamath] Fyi: Linode rebrand

Yikes. That's a tad worrisome. Thanks for these updates. Hetzner has some machines that support Alder Lake's relatively new TME-MK. I've not looked deeply into whether they've exposed that into their products, but it's probably worth looking into if you're particularly security-conscious.

Re: [Metamath] status of nnne0ALT

For what it's worth, here's some git history: $ git log -L '/nnne0ALT \$p/,+1:set.mm' commit df12e3e7168f44afd3771b5aba5286a66f1ae8f6 Author: Steven Nguyen Date: Tue Jan 31 14:18:36 2023 -0600 rename equsb3lem et al to equsb3v et al, rmv ax-mulgt0 from 0nnn

Re: [Metamath] Metamath mirrors: Current state & proposed plan

> > - Tighter sync between mirrors and us.metamath.org > > I don't think that's critical. We update 1/day, and it's not a crisis if > the mirror update is delayed. Also, rsync is *really* fast at determining > "there is nothing to do". Good point. With a slow, prescribed update cadence, this

Re: [Metamath] Metamath mirrors: Current state & proposed plan

Nice work modernizing and hardening the infra. These days what's considered the "bare minimum" has a lot of moving pieces. Anyway, please permit me to butt in with a small idea. The mirror setup you propose has each mirror polling the source server for changes. What about a push-centered

Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over I

This is absolutely beautiful. Congratulations! Incidentally, I just recently re-discovered Schroeder-Bernstein, realizing that I have thoroughly internalized the result without ever attempting a proof. Poking at the latter gave me whiffs of some deeper foundational links, but I just assumed it

Re: [Metamath] Re: Metamath Zero dissertation defense

Congrats, Mario, on making it through a Ph.D. thesis defense! Hope you destroyed the grilling. I would love to have attended, but it was in the middle of the night in my time zone. Will a recording be available as well? Jon P wrote: > Hey Mario, I've been enjoying your thesis and just wanted to

Re: [Metamath] Norman Megill (1950-2021)

Oh no... This is devastating... I am but a lurker here, but the quality of discussions, care of contributors, and sheer fun of playing with metamath are a tribute to the love that Norm poured into this community. What a towering legacy. Though I have only had a few brief e-mail exchanges with

Re: [Metamath] Re: Recommendations for metamath hosting?

FWIW, I can also vouch for DitialOcean and Linode VMs. Both are hosts that my employer makes liberal use of, and it sounds like our egress data distribution is similar to that of us.metamath.org. Norman Megill wrote: > I got the response, " Open Source plans are only applicable for team >

Re: [Metamath] Re: Typo in comment to ~ caov?

Hrm. My set.mm is just from the HEAD of master, which indeed looks old: $ git log -1 --pretty=reference 3921b733 (last release with old axiom numbers, 2018-12-20) Your comment prompted me to look more closely at the repo. I guess the latest set.mm is on the `develop' branch instead? >

[Metamath] Typo in comment to ~ caov?

This is quite trivial, but is the comment to ~ caov correct? "Extend class notation to include the value of an operation ` F ` (such as ` + ` ) for two arguments ` A ` and ` B ` . Note that the syntax is simply three class symbols in a row surrounded by special parentheses

Re: [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI

This is a good point. It's probably a good idea to have different behaviour depending on "interative" vs. "non-interactive" use. Having a mandatory "--interacitev" option seems heavy-handed though. On Linux at least, you can automatically detect "interactive" input by checking if stdout is

Re: [Metamath] Packaging Metamath for Linux distros

Norman Megill wrote: > On Monday, April 27, 2020 at 10:46:41 PM UTC-4, David A. Wheeler wrote: > > > > On Tue, 28 Apr 2020 11:23:08 +0900, heiphohmia via Metamath wrote: > > > Norm, thank you for tagging v0.182 as well as merging the pull request. > >

Re: [Metamath] Packaging Metamath for Linux distros

Norm, thank you for tagging v0.182 as well as merging the pull request. I am getting the impression that this thread has mostly increased your maintenance burden. That's really counter to my intent and needn't be the case! The whole release process on the GitHub side can be made very automatic.

Re: [Metamath] Re: FL: ++; binary connectives

Well, U+2206 (INCREMENT) is the only correctly oriented triangle I see in the Mathematical Operators block (https://codepoints.net/mathematical_operators). The U+25B3 (WHITE UP-POINTING TRIANGE) is part of the Geometric Shapes block (https://codepoints.net/geometric_shapes). Looking at the

Re: [Metamath] Packaging Metamath for Linux distros

Hello Norm, This is in reply to https://groups.google.com/forum/#!searchin/metamath/Packaging$20Metamath$20for$20Linux%7Csort:date/metamath/z2kKJYgnz-g/xmRVy0KhCQAJ For whatever reason my direct replies to the above seem to be falling into Google's black hole, so I am sending this as a new

Re: [Metamath] Re: FL: ++; binary connectives

FWIW, this Wikipedia list corresponds TeX's \triangle with U+2206: https://en.wikipedia.org/wiki/List_of_mathematical_symbols_by_subject Mario Carneiro wrote: > I'm not so sure about that. It looks like the primary meaning of that > codepoint is "increment operator", used for small discrete

Re: [Metamath] Re: FL: ++; binary connectives

Maybe this is just displaying my ignorance, but decimal 97 is ASCII 'a'. Perhaps you mean't 94, which corresponds to the caret (i.e. '^')? Mario Carneiro wrote: > > Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, not > > "concat"); > > > > By the way, I would like to

Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm

Giovanni, Currently, Norm has me assigned to the 113-116. Last email I saw, there were still several other ranges open, however. If that's changed and all slots are allocated, I certainly don't mind sharing my batch. Cheers, Giovanni Mascellani wrote: > Hi, > > first of all, Norm, could you

Re: [Metamath] Full 'minimize' run on set.mm

Okay, I will hold off on 123 and 124. Mario Carneiro wrote: > I'm trying out 123 and 124 for now using AWS. I might be able to scale up > depending on the results. > > On Thu, Feb 13, 2020 at 4:51 PM David Starner wrote: > > > On Thu, Feb 13, 2020 at 2:28 PM Norman Megill wrote: > > > > > >

Re: [Metamath] Updated "jobs" scripts available for full 'minimize' run on set.mm

"David A. Wheeler" wrote: > I've just posted an updated "jobs" system if you want to do > big-scale minimization, especially if you're using a number of cores. > > This version supports disjoint sets of jobs, e.g., you can now say: > scripts/jobs 112 125-132 144-151 > That means the API has

Re: [Metamath] Full 'minimize' run on set.mm

Alexander van der Vekens wrote: > On Thursday, February 13, 2020 at 7:22:58 AM UTC+1, heiph...@wilsonb.com > wrote: > > > > The problem was on my end. The build system I was using ended up lying > > about > > deleting the old zip. Manually removed and I see 0.181 now. > > > > Are 101 and 102

Re: [Metamath] Full 'minimize' run on set.mm

The problem was on my end. The build system I was using ended up lying about deleting the old zip. Manually removed and I see 0.181 now. Are 101 and 102 still open now? If so, I will take them. Otherwise, my stake is on the next two lowest ordinals. Norman Megill wrote: > On Thursday, February

Re: [Metamath] Full 'minimize' run on set.mm

Thank you, Norm. I am now seeing the 0.181 in metamath-program.zip. Norman Megill wrote: > On Thursday, February 13, 2020 at 12:14:44 AM UTC-5, Alexander van der > Vekens wrote: > > > > I also tried several URLs, but always get Version 0.180 (and tested it > > with minimizing axdc - the proof

[Metamath] A wrapper script for the metamath executable

This is something I would just like to share. Please let me know if you find this helpful. Attached is a wrapper script around the metamath executable that provides the following: - Automatic setting of height and width from terminal (if tput is found), - Automatic execution with rlwrap (again,

Re: [Metamath] Re: metamath-program.zip archive getting ninja edited

> In the meantime, I have stopped regenerating > http://us.metamath.org/downloads/metamath-program.zip each site build. Thank you. This is very much appreciated. However, I feel bad that this ended up simply creating mork work for you. If there is any way I can help automate things, please

Re: [Metamath] Re: metamath-program.zip archive getting ninja edited

> I tested it, and tar.bz2 seems stable but tar.gz changes its md5sum each > time I run tar -czf. Hrm. Both Nix and Guix rely on the fact that tar.bz2, tar.gz, and tar.xz can be made deterministic. However, this is starting to do down the reproducible builds rabbit hole, which is deep. Here is

[Metamath] metamath-program.zip archive getting ninja edited

This is part of a larger discussion happening at [1]. It appears that the metamath-program.zip URL[0] points to a non-static archive. Sadly, this is preventing me from packaging metamath for my Linux distribution. Just for the sake of clarity, below are the SHA-256 sums of the archive retrieved

Re: [Metamath] Packaging Metamath for Linux distros

> Maybe you can let me know exactly what files you'd like to see in it. Thank you for engaging so openly. Personally, my preferences align mostly with FL's. As a Linux user, the default expectation I have for a source tarball (in this case metamath-program.zip) is that I can do $

Re: [Metamath] Packaging Metamath for Linux distros

> And why not a special Linux source distribution... The URL that Norm shared pretty much ticks all the boxes you outline. The only substantive difference being that the metamath.exe is not excluded. The source uses GNU autotools, so the standard build procedure Just Works if you first generate

Re: [Metamath] Packaging Metamath for Linux distros

that Norm also keeps old versions of the tarball with names > indexed by date, although I don't know if the dated copies include the most > recent version or only start at the second most recent version. Norm will > have to give the details on this. > > Mario Carneiro > > On Fri, Dec 1

[Metamath] Packaging Metamath for Linux distros

Dear Metamath, This outlines some of the issues I encounterd when attempting to package up metamath for Void Linux. Need to make metamath more available! The content here essentially reiterates that of a previous post of mine, which just happened to go out right before the DNS debacle, causing

[Metamath] oveq2i has logical hypothesis named oveq1i.1

Hello, The logical hypothesis for theorem oveq2i has the same name as that for oveq1i. This tripped me up, but is the naming intentional? In particular, I was writing up my own proof of 2p2e4 when I noticed the clash. In fact, the proof of 2p2e4 exhibits the same exact issue: the first

[Metamath] Deduction oveq2i has logical hypothesis named oveq1i.1

Hello, The names in the subject line tripped me up. Is this intentional? In particular, looking at the proof 2p2e4, the first unification is oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. The mismatch between the deduction name and its hypothesis name confused me for a bit.

[Metamath] Deduction oveq2i has logical hypothesis named oveq1i.1

Hello, The names in the subject line tripped me up. Is this intentional? In particular, looking at the proof 2p2e4, the first unification is oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. The mismatch between the deduction name and its hypothesis name confused me for a bit.