[Metamath] Updated Gource visualization now public!

The video "Metamath Proof Explorer (set.mm) contributions visualized with Gource through 2020-04-29" is now available at: https://www.youtube.com/watch?v=LVGSeDjWzUo This is a view of the contributions to the Metamath Proof Explorer (MPE) (aka set.mm) database using Gource through 2020-04-29.

Re: [Metamath] Proposed installation conventions so things will be easier to install

Forwarded Message Subject: Current problem Date: Tue, 5 May 2020 20:19:24 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this. I don't know how you do, but my own version of mmj2 has no problems to find set.mm in the current directory. -- FL On Tuesday, May

Re: [Metamath] Proposed installation conventions so things will be easier to install

On Tue, 5 May 2020 08:00:35 -0700, David Starner wrote: > It'd be a lot easier to handle set.mm if it were more standard to have > set.mm as a constant and editing being done to separate .mm files. I don't think so. Which version of set.mm would be constant? --- David A. Wheeler -- You

Re: [Metamath] Proposed installation conventions so things will be easier to install

It'd be a lot easier to handle set.mm if it were more standard to have set.mm as a constant and editing being done to separate .mm files. -- The standard is written in English . If you have trouble understanding a particular section, read it again and again and again . . . Sit up straight. Eat

Re: [Metamath] Proposed installation conventions so things will be easier to install

FL: > For me it's not "/usr/bin" it's "/usr/local/bin" That's true for many people. Metamath-exe actually already supports this, just use "make install" with autoconf (as always that's the default). If you want /usr/bin (as is common for packages installed with a package manager), use

Re: [Metamath] Re: Proposed installation conventions so things will be easier to install

On Mon, 4 May 2020 23:58:46 -0700 (PDT), savask wrote: > I just wanted to make a small comment, based on personal experience. > > Back when I first tried metamath, I found it very convenient that it was > shipped as a standalone executable. I don't really like programs which > "clutter" the

Re: [Metamath] Proposed installation conventions so things will be easier to install

Forwarded Message Subject: Directories Date: Tue, 5 May 2020 11:36:00 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this. For me it's not "/usr/bin" it's "/usr/local/bin" and set.mm is not a library it's a file of data. You have to be able to browse it and

[Metamath] Re: Calculational rendering of Metamath proofs, using Greasemonkey/Firefox

Hi all, Last week, I've made a number of updates (dare I say improvements?) to my 'userscript' mm-calc2 (link to latest version, currently at version 7). It still does essentially the same thing, namely

[Metamath] Re: Proposed installation conventions so things will be easier to install

I just wanted to make a small comment, based on personal experience. Back when I first tried metamath, I found it very convenient that it was shipped as a standalone executable. I don't really like programs which "clutter" the home directory or make some unasked changes to the file system