Generate `discouraged` file

[tirix]

This adds a -D or --discouraged flag to the command line version of the tool to generate the discouraged file, in the same format as metamath.exe.

[tirix]

There is currently a discrepancy in the number of steps mentioned in the Proof modification of "XXX" is discouraged (X steps)., the metamath-knife calculation has sometimes fewer steps than metamath.exe.

Some random examples below:

• id1 : metamath.exe : 5 steps, metamath-knife : 2 steps
• p0exALT : metamath.exe : 5 steps, metamath-knife : 2 steps
• prel12gOLD : metamath.exe : 332 steps, metamath-knife : 329 steps
• psgnunilem5OLD : metamath.exe : 1060 steps, metamath-knife : 1054 steps
• usgrnbnself2OLD: metamath.exe : 7 steps, metamath-knife : 4 steps

Looking at the minimal examples, it looks like metamath.exe would be in the wrong (id1 obviously only has 2 steps, I don't see where the 3 additional steps might be coming from).

[tirix]

Note that it's possible to set the --timing flag to measure the CPU time spent on building the discouraged file. My computer runs it in around 2s, that would be roughly a 10 fold improvement vs. 23s for metamath.exe.

[digama0]

There is currently a discrepancy in the number of steps mentioned in the Proof modification of "XXX" is discouraged (X steps)., the metamath-knife calculation has sometimes fewer steps than metamath.exe.

I can't replicate. I tried running metamath.exe on id1 (both a standalone test case and the one in set.mm) and got 2 steps in both cases, and the discouraged file in set.mm repo also shows 2 steps for id1. Same thing for the other theorems mentioned. In any case, it is more important to match the counts used in the repo (which I think are being generated by mmj2 because metamath.exe is too slow).

[digama0]

I think you got the labels mixed up. I am able to observe a difference now, but it is metamath-knife that is generating the incorrect numbers, not metamath-exe / mmj2 (which seem to agree). For example they both think id1 is 2 steps while metamath-knife is reporting 5 steps.

[digama0]

2 seconds also sounds a bit slow considering what it is doing. I pushed a version that just scans the labels in the paren list in order to count steps, and now it is down to 0.5 seconds to generate the file, and it is also generating the correct numbers. (The bug in your implementation was that it was counting each occurrence of 'A'..='T' as a step, including inside the paren list, which is why ( idALT ) AB looks like five steps instead of two (for A,L,T,A,B).)

[tirix]

Excellent, thanks a lot!

[tirix]

I've had a closer look at how this is used and we need to generate two different files, one for iset.mm and one for set.mm. The file name discouraged is currently hard-coded, I'll change that to be a parameter.

[benjub]

FYI @tirix:

~/Documents/_metamath/git/metamath-knife (main) $ cargo build --release
error: failed to parse manifest at `/home/benoit/Documents/_metamath/git/metamath-knife/Cargo.toml`

Caused by:
  failed to parse the `edition` key

Caused by:
  this version of Cargo is older than the `2021` edition, and only supports `2015` and `2018` editions.
~/Documents/_metamath/git/metamath-knife (main) $ uname -a
Linux ordi 5.10.0-21-amd64 #1 SMP Debian 5.10.162-1 (2023-01-21) x86_64 GNU/Linux
~/Documents/_metamath/git/metamath-knife (main) $ cargo --version
cargo 1.46.0

(I installed cargo using apt.) Anyway, I already had to update Debian, so I guess this is another incentive to do so !

[digama0]

You should generally avoid installing rustc / cargo using apt, because this lags considerably behind the last stable release. (It sounds like your version is older even than that, though.) You should use https://rustup.rs to get the rustup program, which is used in turn to manage (get and update) various versions of rustc and cargo.

[benjub]

Thanks. FYI:

~/Documents/_metamath/git/metamath-knife (main) $ cargo build --release
[...]
 Finished release [optimized + debuginfo] target(s) in 1m 13s
~/Documents/_metamath/git/metamath-knife (main) $ target/release/metamath-knife --timing --jobs 4 --split --verify ../set.mm/set.mm
parse 75ms
nameck 26ms
scopeck 3532ms
verify 148ms
diag 0ms
0 diagnostics issued.

[digama0]

That scopeck timing sounds abnormally large. It seems that using --split significantly increases the time needed for scopeck, I'm not sure why.

[tirix]

You should use https://rustup.rs to get the rustup program, which is used in turn to manage (get and update) various versions of rustc and cargo.

We should probably mention that in the README.md, it currently mentions Rust 2018.

[tirix]

Also, it would be nice to e.g. copy/paste the output of --help into README.md, to show all different possible options.

[benjub]

Also, it would be nice to e.g. copy/paste the output of --help into README.md, to show all different possible options.

BTW @tirix : in that output, two occurrences of "Prints" should be "Print".