> 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. 
>
>
I know perfectly well that the package currently available is perfectly 
usable. I simply point out that as long as you are dealing with linux 
distributions, the easiest way is to respect the standards specific to 
Linux source distributions: a configure (already generated by autoreconf) a 
README, an INSTALL, a Makefile. Everything that a person who installs a 
source on Linux expects to find. And no Windows hardware (we don't put the 
devil in the church!)

 

> The source uses GNU autotools, so the standard build procedure Just Works 
> if 
> you first generate the necessary files with 
>
>     $ autoreconf -i 
>
> I do find it curious that the advice for *nix builds is to directly call 
> gcc. 
> Perhaps the build instructions could be updated to this: 
>
>     $ autoreconf -i && configure && make 
>
>
It should be uptated to that:

configure && make && make install

 

> The TeX source for the metamath book is located here[0]. Said URL is 
> already 
> prominently on the homepage, and I 
>
> [0]:http://us.metamath.org/latex/metamath.tex 
>
>
Okay, but I just want to point out that, if we' re going to do anything, we 
might as well put the TeX file in the source distribution. Documentation is 
always part of the source documentation.

 

> This reads to me like it is suggesting users generate set.mm. Since that 
> doesn't really make sense, I assume that I am just misreading something. 
>
>
It makes sense. Not everyone is connected 24 hours a day to the Internet. 
You may prefer that your computer is not likely to be hacked by smart 
people. Knuth never puts his computers on the Internet.

You may also want to have several successive states of the database. I must 
have half a dozen of them installed on my computer.

You may prefer to stay offline to cure your Internet addiction. 

You may want to think about the planet and relieve the network. The 
Internet consumes as much energy as aeronautics because of all the 
advertising and netflix crap that goes through it.

-- 
FL

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to [email protected].
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/77a6ba68-26d6-4d32-8d9f-2e0a47c6fb14%40googlegroups.com.

Reply via email to