> 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 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

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

> And also tips on finding the associated database and a procedure to recreate
> it on a personal computer...

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.


"'fl' via Metamath" <[email protected]> wrote:

>
> And why not a special Linux source distribution, a gzipped tarball, without 
> Windows executable, 
> without database, but with the manual page, the TeX file of the manual, the 
> Makefile, a configure.ac, 
> and a "configure" program. In short, the standard source distribution for 
> Linux like the tar.gz on this page:
>
> https://github.com/coq/coq/releases/tag/V8.10.2
>
> With a static link so that special distributions packagers can easily find 
> it. And also tips on finding 
> the associated database and a procedure to recreate it on a personal 
> computer with a warning message 
> to explain to the reckless user that it will take a very long time to get 
> it and that s.he might prefer using the
> already compiled one on the net.
>
> -- 
> 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/7fba4251-4fe3-4578-b103-8c07f29dcf76%40googlegroups.com.

-- 
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/5df787b8.bnsW1w9XsY9RsYfU%25heiphohmia%40wilsonb.com.

Attachment: sig.asc
Description: application/pgp-encrypted

Reply via email to