File import $[ $] command spec change

[Mario Carneiro]

Hello all,

I'm writing to suggest a change to the Metamath spec regarding the file name path in an import statement. Currently, the file syntax uses a backslash and is relative to the working directory from which you ran metamath or mmj2. This is not very portable, since this means that if you try to run metamath from another directory and access the same .mm file, you have to go in to the .mm file and change any import statements to be relative to the new path. Wouldn't this make a lot more sense if the file path was relative to the file that contained the import statement? Or at least it could check both locations in a sort of PATH mimic.

Also, the use of backslashes is not very portable to non-windows systems. Could we use a forward slash a la linux and web URLs?

Mario

[Norman Megill]

On Saturday, December 20, 2014 7:57:35 PM UTC-5, Mario Carneiro wrote:
>  I'm writing to suggest a change to the Metamath spec regarding the file
>  name path in an import statement.  Currently, the file syntax uses a
>  backslash and is relative to the working directory from which you ran
>  metamath or mmj2.  This is not very portable, since this means that if
>  you try to run metamath from another directory and access the same .mm
>  file, you have to go in to the .mm file and change any import statements
>  to be relative to the new path.  Wouldn't this make a lot more sense if
>  the file path was relative to the file that contained the import
>  statement?  Or at least it could check both locations in a sort of PATH
>  mimic.

I think this is a reasonable idea, although I'm not sure how much should
be in the spec vs. the implementation.  Similar to the C language and
most language specs, I think, the Metamath spec leaves such things like
case sensitivity of file names undefined because they are OS-dependent.

I'm willing to change the metamath program (in an ANSI-compliant way)
to accommodate this.  Would something like "use the directory prefix of
the starting file unless the included file has a directory prefix" be
what you want?  I could also try both the local and directory-prefixed
include files can be done, but which should be tried first, and should
the user be warned if both exist?  (I've been tricked by PATH picking up
the wrong version of something under Windows, where every application
thinks they own the system and permanently adds more directories to
PATH.)

>  Also, the use of backslashes is not very portable to non-windows
>  systems.  Could we use a forward slash a la linux and web URLs?

The metamath.c code currently passes the user's string directly to fopen
as is, but the compilers I've been using on Windows (gcc and clang under
Cygwin, and lcc) all accept either forward or backward slash.  I didn't
check mmj2.

Curiously, gcc opens the file in "Unix mode" (not ignoring carriage
returns) if backslashes are used.  I think this is a Cygwin thing.  The
metamath program cleans them out to prevent double spacing upon 'write
source'.

    MM> read '../mm/set.mm'
    Reading source file "../mm/set.mm"...
    367360 lines (19767531 characters) were read from "../mm/set.mm".
    The source has 100203 statements; 1772 are $a and 21311 are $p.
    No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
    if you want to check them.
    MM> erase
    Metamath has been reset to the starting state.
    MM> read '..\mm\set.mm'
    Reading source file "..\mm\set.mm"...
    ?Warning: the source file has carriage-returns.  Cleaning them up...
    367360 lines (19767531 characters) were read from "..\mm\set.mm".
    The source has 100203 statements; 1772 are $a and 21311 are $p.
    No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
    if you want to check them.

Norm

[fl]

mmj2 opens the file in the current directory and doesn't accept anything else.

Well the old version. I don't use the new one because it is buggy and not even released

to be frank.

-- 

FL

[fl]

Well the old version. I don't use the new one because it is buggy and not even released

to be frank.

It is unfortunate: it was a very good program and it deserved to be correctly maintained.

-- 

FL

[Mario Carneiro]

I don't have a good suggestion here. Would it be too confusing to use a leading slash as a sort of "project root" meaning and use the current algorithm for such paths and file-relative paths for those without leading slashes?

 

>  Also, the use of backslashes is not very portable to non-windows
>  systems.  Could we use a forward slash a la linux and web URLs?

The metamath.c code currently passes the user's string directly to fopen
as is, but the compilers I've been using on Windows (gcc and clang under
Cygwin, and lcc) all accept either forward or backward slash.  I didn't
check mmj2.

Looking at your examples below, I realized that "read mm/set.mm" may be failing not due to refusal of the forward slash, but rather the command-line parser treating the last bit as an option rather than a file name. Is it a possibility to treat it as part of a file name if it doesn't match an option?

On Tue, Dec 23, 2014 at 10:38 AM, fl <freder...@laposte.net> wrote:

mmj2 opens the file in the current directory and doesn't accept anything else.

I'm aware. That's why I started this thread -- I can't change something like that directly, because it has to do with spec compliance, so the spec needs to change and both the metamath and mmj2 programs need to be patched.

Well the old version. I don't use the new one because it is buggy and not even released

to be frank.

Please don't complain about bugs if you aren't using the latest version. I'm doing my best, but let me remind you that this is essentially volunteer work; I'm not getting paid for any of this, so keep in mind that some things may take time to accomplish depending on my priorities. Also, it's always an option to patch it yourself, and put your effort where you mouth is. I can't address generic complaints.

As for "not released", I had been waiting on the completion of the autocompletions branch by Alexey. It's still not as complete as I'd like, but I guess he's done with it for now, so I'll work on getting an actual release out soon.

It is unfortunate: it was a very good program and it deserved to be correctly maintained.

You're right, it would be great if ocat was still here and could maintain his program. Unfortunately he's not, and at least with me there is a chance of new features being added and bugs being fixed. Again, if you want you can step up to the plate yourself, but I'm sure that's not what you mean.

Mario

[fl]

Please don't complain about bugs if you aren't using the latest version.

Is is impossible to use something that is buggy. And I don't complain I regret that's all.

-- 

FL

[Mario Carneiro]

On Tue, Dec 23, 2014 at 12:07 PM, fl <freder...@laposte.net> wrote:

Please don't complain about bugs if you aren't using the latest version.

Is is impossible to use something that is buggy. And I don't complain I regret that's all.

Being a mathematician as well as a programmer, I use the program in its latest version quite extensively with few difficulties. I'm assuming that your issues are genuine bugs and not a misunderstanding in the use of the software; in either case, you should probably be more specific about what problems you are encountering (on a different thread). Merely saying that the program is "buggy" without additional evidence or details is not helpful or useful to anyone.

Mario

[Mario Carneiro]

FL's post is reproduced below.  As group manager I deleted it since IMO
it did not add value to the discussion.  However, since FL objected, I
am restoring his message from my inbox (since Google has no undelete)
and will let it speak for itself.

On Wed, Dec 24, 2014 at 4:18 AM, fl <freder...@laposte.net> wrote:

Being a mathematician as well as a programmer,

That's the problem, I think.

--
FL

[Norman Megill]

Here is a proposal for the metamath program.

1. When starting a 'read' command, save any directory prefix from the file name.  The prefix is defined as the string up and including the last forward or backward slash.

2. Upon encountering an include directive $[...$], first check whether the included file exists as is, if so use it.  Otherwise, if the file name has no directory prefix, and the main file name does, check whether the included file exists with the directory prefix.  Otherwise, provide an error message.

The order of checking in step 2 will make the program's behavior match the existing program when the included file is present.  If the included file isn't present (which would be an error condition in the existing program), it will then try the directory of the main file.  Please consider your use cases to make sure this is behavior that makes the most sense.

----

Regarding quoting the file name, from 'help read':  "Note that in Unix, any directory path with /'s must be surrounded by quotes so Metamath will not interpret the / as a command qualifier."  Also, 'help invoke' gives conditions under which the file name must be quoted when used as command-line arguments.

Note that a trailing quote is optional:  "read 'abc/set.mm" will have an implicit trailing quote added when preprocessing the command line.

Quotes are needed around any command-line argument (file name or otherwise) that contains space, /, or =. The characters / and = are special in that spaces are put around them for command-line preprocessing unless they are inside of quotes.  This was done for user convenience since these two characters are so often used.  See 'help cli' for more information.

I considered making the command qualifier character ot the Unix "-" rather than the VAX and DOS "/" when things transitioned to Unix, but that would mean we would have to quote many labels; for example, 'show statement ax-mp/comment' would become 'show statement "ax-mp"-comment'.

Norm

[Stefan O'Rear]

On Saturday, December 20, 2014 4:57:35 PM UTC-8, Mario Carneiro wrote:

I'm writing to suggest a change to the Metamath spec regarding the file name path in an import statement. Currently, the file syntax uses a backslash and is relative to the working directory from which you ran metamath or mmj2. This is not very portable, since this means that if you try to run metamath from another directory and access the same .mm file, you have to go in to the .mm file and change any import statements to be relative to the new path. Wouldn't this make a lot more sense if the file path was relative to the file that contained the import statement? Or at least it could check both locations in a sort of PATH mimic.

Also, the use of backslashes is not very portable to non-windows systems. Could we use a forward slash a la linux and web URLs?

What sorts of things do people here use file inclusion for?  I have a working copy of my mathbox, by itself, with a $[ set.mm-with-all-mathboxes-removed $] at the top, to avoid vim and git getting slow with a 17MB file... although I'm probably going to have to break it up into N files soon because the problem is coming back.

I'm not a big fan of the way $[ $] works in general.  I've been mulling ideas for another Metamath-file-processing program, and it seems extremely difficult to do anything useful with $[ $], because it can appear practically anywhere.  It's fine on reading, but if you want to write out a system of .mm files the way they were read in, how could you handle a $[ $] in the middle of the token list of an $a or $p statement?  Just as an example.

So I'd like to invite a discussion on how $[ $] is used.  Which subsets of it are important to support, and would it be a good idea to have something that isn't a subset at all?  What tools for organization do we want to have when the $p count breaks 100k?

-sorear

[Norman Megill]

On 12/29/14 3:02 AM, Stefan O'Rear wrote:
> On Saturday, December 20, 2014 4:57:35 PM UTC-8, Mario Carneiro wrote:
>
>     I'm writing to suggest a change to the Metamath spec regarding the
>     file name path in an import statement. Currently, the file syntax
>     uses a backslash and is relative to the working directory from which
>     you ran metamath or mmj2. This is not very portable, since this
>     means that if you try to run metamath from another directory and
>     access the same .mm file, you have to go in to the .mm file and
>     change any import statements to be relative to the new path.
>     Wouldn't this make a lot more sense if the file path was relative to
>     the file that contained the import statement? Or at least it could
>     check both locations in a sort of PATH mimic.
>
>     Also, the use of backslashes is not very portable to non-windows
>     systems. Could we use a forward slash a la linux and web URLs?
>
>
> What sorts of things do people here use file inclusion for?

I haven't used the $[ $] inclusion in a long time.  I once tried using it to have a hierarchy of modules such as logic.mm, zfc.mm, complex.mm, etc., but maintaining separate files for things like global label changes was annoying, and it ended up much easier to maintain a single file.  Of course, this can't continue indefinitely as set.mm grows.

> I have a
> working copy of my mathbox, by itself, with a $[
> set.mm-with-all-mathboxes-removed $] at the top, to avoid vim and git
> getting slow with a 17MB file... although I'm probably going to have to
> break it up into N files soon because the problem is coming back.
>
> I'm not a big fan of the way $[ $] works in general.  I've been mulling
> ideas for another Metamath-file-processing program, and it seems
> extremely difficult to do anything useful with $[ $], because it can
> appear practically anywhere.  It's fine on reading, but if you want to
> write out a system of .mm files the way they were read in, how could you
> handle a $[ $] in the middle of the token list of an $a or $p statement?
>   Just as an example.
>
> So I'd like to invite a discussion on how $[ $] is used.  Which subsets
> of it are important to support, and would it be a good idea to have
> something that isn't a subset at all?  What tools for organization do we
> want to have when the $p count breaks 100k?

An idea I've been toying with for a while involves two commands that would be added to the metamath (or other) program, EXTRACT and MERGE.  Conceptually, these are very sophisticated extensions of WRITE SOURCE and READ respectively.

EXTRACT <label-list> <out-file>
MERGE <inp-file> <inp-file>

EXTRACT would be given a theorem or list of theorems, recursively determine what they depend on, and produce a set.mm subset with exactly and only the axioms, definitions, and theorems needed.  Little details would need to be paid attention to like keeping section headers whenever a theorem from that section is used, keeping comments intact, cleanly breaking out theorems sharing common $e's, keeping relevant htmldefs, and overall maintaining the formatting conventions used in set.mm.  For example,

MM> read set.mm
MM> extract ax-resscn~cju complex.mm

would create the file "complex.mm" with exactly and only the set.mm subset needed for basic complex number theory i.e. for statements ax-resscn through cju.  This file will be much smaller that the whole of set.mm, and work could continue on it independently of the rest of set.mm.  If we also want to make sure that all prop calc theorems are available in complex.mm, just in case useful ones were missed because they weren't needed, we can do

MM> extract ax-1~trud,ax-resscn~cju complex.mm

MERGE would take two .mm's and reassemble a .mm containing both.  The two .mm's could be two extractions, an edited extraction and the original set.mm, or even two set.mm's that were independently edited.

The first .mm would be "primary", meaning its labels, comments, and tokens would dominate (take precedence).  In the ideal case, theorems would be matched by content, not labels (ideally even tolerating variable renaming), and in that case the primary file's label and variable names would be used.  When there is a label conflict (same label for different theorems), the label in the secondary file, say abc.mm, would be suffixed with the file name, say "_abc.mm", which can be cleaned up by hand later.  Conflicting tokens (a token with a different definition in each file) could be handled similarly.

If two theorems are the same with different proofs, we would use the proof requiring fewer axioms, or if the same axioms are used, the one with the shortest proof.

Sections would be matched up as best possible, based on the section name and section identifying conventions ("=-=-=-" etc.).  The final output would be a valid .mm file no matter what, and a warning list would guide the user for what needed to be cleaned up by hand.  For example,

MM> erase
MM> merge complex.mm set.mm

would read and internally merge the two files, and the result can be written out with the usual 'write source' (or even 'extract').  In the above example, complex.mm would take precedence in case of renamed labels, changed comments, etc., whereas in

MM> merge set.mm complex.mm

the input file set.mm would take precedence.

Note that (ideally) 'merge set.mm set.mm' would be equivalent to 'read set.mm', and 'extract * set.mm' would be equivalent to 'write source set.mm'.

I think these commands could make a significant difference because people can work with smaller set.mm pieces or even the whole set.mm independently, without much concern of clashes with what others are doing.  No changes to the Metamath language are required.

I can envision a time in the future when mathematicians can share theorems by extracting and merging what they are interested in rather than depending on a huge master set.mm, most of which would not be of interest to them.

Norm