Hi Zheng Fan,
I'd be glad to help you use and understand that program. There were
several new developments since that email, and my personal fork might
not have been up-to-date, can you please try again with the code on
David's branch?
https://github.com/david-a-wheeler/metamath-knife
I hope that project will soon be in a state where it can be moved to the
set.mm GitHub organization!
Also, could you please point me to the version of set.mm and the command
line parameters you're using, so that I can try to reproduce the issue?
In order to avoid bothering this list with our possible back-and-forth
trying to pinpoint the root cause of the issue, you could also open an
issue in that GitHub repository, and we can keep our exchanges there.
A better description of the algorithm is due, I tried to introduce it in
one of my posts
<https://groups.google.com/g/metamath/c/x52J7yjl5iA/m/cUqhdJHdBQAJ> here.
More generally, thank you very much for the attribution, but as the
thread title suggests, the idea is to build a community verifier. I
would not like to see this project as mine but rather as the
community's. This is really actually a community work starting from
Stefan O'Rear's foundaments, with major contributions from Mario and
David. In his original post, Mario expressed his wish to avoid
fragmentation in the community.
/The plan is to start a new "community verifier" and build it with
those tasks in mind. I think there has been too much fragmentation in
verifier land; this makes it very hard for newcomers, especially those
that are not especially computer literate such as traditional
mathematicians./
So the spirit would rather be that instead of building your own
verifier/proof assistant, you're welcome to contribute to this community
project :-)
BR,
_
Thierry
On 05/11/2021 06:44, Zheng Fan wrote:
Hi all,
I downloaded Thierry Arnoux's metamath-knife repo and ran it on a
version of set.mm (not the current one), and it runs for 10+ min
without any output. It is really weird in that I ran it on the
predicate fragment (set-pred.mm) and it finishes in a fraction of a
second. Could you help me figure out why? I am writing a metamath
parser myself and I want to borrow some ideas from your
implementation. Is there a write-up of a high-level overview of the
algorithm used? Thanks very much.
在2021年8月15日星期日 UTC+2 下午3:23:56<Thierry Arnoux> 写道：
Hi Stefan, David and all,
Eight months after this discussion was launched I have made what I
think is an important breakthrough: the "grammar" addition to SMM3
/ metamath-knife can now parse all statements of set.mm
<http://set.mm>, including the complex ones where look ahead is
required, into tree-like "formula" structures. Code is as always
available on my fork
<https://github.com/tirix/metamath-knife/tree/grammar> for those
interested.
On my MacBookPro 2015, parsing the full database takes around 3s
on one single thread, and 1s when multi-threaded. This is roughly
the same cost as the "scopeck" step. Building the grammar for the
parsing, based on the syntactical axioms, only takes around 13ms.
I was surprised how easy it was to introduce multi-threading.
I believe this is the first step to make `metamath-knife` a
library for a new community proof assistant. I want to continue to
evolve the resulting "Formula" structure so that it supports basic
functionalities such as substitution and unification. However I
don't want to go too far beyond that, I think further
functionality shall be placed in the "application" part.
Stefan, David, I would like to soon move on pulling this code into
an official rust crate. You own the repositories for `smetamath`,
respectively `metamath-knife`.
How could we proceed?
Specifically:
* I believe the 'statement parsing' functionality shall be part
of a basic Metamath library. Do we have an agreement here?
This would mean I could go ahead an issue a PR :-)
* Which repository shall be used and evolve? Stefan's
`smetamath <https://github.com/sorear/smetamath-rs>`, or
David's `metamath-knife
<https://github.com/david-a-wheeler/metamath-knife>` ?
* Since there was broad agreement to build a community project
on Rust, could we move the repository into GitHub's Metamath
organization <https://github.com/metamath>? Norm, would you agree?
BR,
_
Thierry
PS. smetamath's TODO <https://crates.io/crates/smetamath#todo>
lists both /grammatical parser/ (the topic of this mail), and also
/outline inference/: I've also added outline inference in the
branch 'outline
<https://github.com/tirix/metamath-knife/blob/outline/src/outline.rs>'.
--
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/88c026c9-f20a-4651-ac86-4d138662a8c4n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/88c026c9-f20a-4651-ac86-4d138662a8c4n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/5390b5fb-3373-65f3-3703-a8416ff9c5c1%40gmx.net.
