Announcing mmpp
127 views
Skip to first unread message
Giovanni Mascellani
Mar 25, 2018, 3:32:45 AM3/25/18
to metamath
Dear Metamath users,
I would like to make you aware of my recent progress on my personal
Metamath project, which is mmpp:
https://github.com/giomasce/mmpp
Mmpp (Metamath in C++) is a tentative new Metamath proof editing
environment, that tries to address those that I perceive as defects on
mmj2, most notably the text only user interface and the lack of proof
automation, which requires the user to spend a lot of time in boring
details instead of in actual mathematics. My ultimate target would be a
tool that optimizes as much as possible the amount of mathematics that
can be formalized per time unit, accepting to compromise on the
aesthetics and minimality of the proofs (both in terms of step number
and axiom usage). Well, I appreciate that there are people who see
things differently, so if this is not your point of view, maybe mmpp
might not be your ideal tool.
That said, I am still far from this ultimate goal, and in some aspects
mmpp is not even on par with mmj2. But it begins to have some usability,
so if anyone wants to try it and give opinions and suggestions (or even
help with coding), everything is welcome. By the way, mmpp is actually
developed with set.mm in mind. While I try to maintain every component
as general as possible, all non trivial algorithms depend fundamentally
on how set.mm is structured.
So far the main mmpp component is called webmmpp and is a web interface
not dissimilar to mmj2 in line of principle, but trying to leverage
modern HTML/CSS/JS to have a richer interface (in particular, it shows
the althtml versions of the steps you input) and featuring fancier
inference rules then the usual Metamath unification. In particular, at
the moment it supports automatically proving inferences which require
purely propositional reasoning (by converting the inference in a CNF and
then using a SAT solver) and a toy implementation of the machine
learning algorithm described in arXiv:1608.02644 (so toy that it does
not have any actual machine learning yet; this will require more work;
however, it pops in every now and then and is still able to save you a
few keyboard strokes).
I am also experimenting with other theorem provers, like Z3 and the
various TSTP solvers. Nothing usable at this point, though. Also, in
line of principle many automation rules can be written for many usual
Metamath gadgets, like substituting a subexpression, automatically
proving that some variable is non free, doing arithmetic and so on.
Eventually I will try to do that and see what happens in terms of
optimizing the proof writing speed.
If you want to try mmpp, please look at the instructions on the webpage
above. I tries to make them as complete as possible and support all
major operating systems. I look forward to hearing your thoughts, both
on the ideas and on the implementation.
Also keep in mind that many advanced features of mmpp require some
support in the underlying set.mm theory, so you will need to use my fork at:
https://github.com/giomasce/set.mm/tree/develop
Thanks and all the best, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles
I would like to make you aware of my recent progress on my personal
Metamath project, which is mmpp:
https://github.com/giomasce/mmpp
Mmpp (Metamath in C++) is a tentative new Metamath proof editing
environment, that tries to address those that I perceive as defects on
mmj2, most notably the text only user interface and the lack of proof
automation, which requires the user to spend a lot of time in boring
details instead of in actual mathematics. My ultimate target would be a
tool that optimizes as much as possible the amount of mathematics that
can be formalized per time unit, accepting to compromise on the
aesthetics and minimality of the proofs (both in terms of step number
and axiom usage). Well, I appreciate that there are people who see
things differently, so if this is not your point of view, maybe mmpp
might not be your ideal tool.
That said, I am still far from this ultimate goal, and in some aspects
mmpp is not even on par with mmj2. But it begins to have some usability,
so if anyone wants to try it and give opinions and suggestions (or even
help with coding), everything is welcome. By the way, mmpp is actually
developed with set.mm in mind. While I try to maintain every component
as general as possible, all non trivial algorithms depend fundamentally
on how set.mm is structured.
So far the main mmpp component is called webmmpp and is a web interface
not dissimilar to mmj2 in line of principle, but trying to leverage
modern HTML/CSS/JS to have a richer interface (in particular, it shows
the althtml versions of the steps you input) and featuring fancier
inference rules then the usual Metamath unification. In particular, at
the moment it supports automatically proving inferences which require
purely propositional reasoning (by converting the inference in a CNF and
then using a SAT solver) and a toy implementation of the machine
learning algorithm described in arXiv:1608.02644 (so toy that it does
not have any actual machine learning yet; this will require more work;
however, it pops in every now and then and is still able to save you a
few keyboard strokes).
I am also experimenting with other theorem provers, like Z3 and the
various TSTP solvers. Nothing usable at this point, though. Also, in
line of principle many automation rules can be written for many usual
Metamath gadgets, like substituting a subexpression, automatically
proving that some variable is non free, doing arithmetic and so on.
Eventually I will try to do that and see what happens in terms of
optimizing the proof writing speed.
If you want to try mmpp, please look at the instructions on the webpage
above. I tries to make them as complete as possible and support all
major operating systems. I look forward to hearing your thoughts, both
on the ideas and on the implementation.
Also keep in mind that many advanced features of mmpp require some
support in the underlying set.mm theory, so you will need to use my fork at:
https://github.com/giomasce/set.mm/tree/develop
Thanks and all the best, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles
Thierry Arnoux
Mar 25, 2018, 9:33:56 PM3/25/18
to meta...@googlegroups.com, Giovanni Mascellani
Hi Giovanni,
This sounds very promising!
I've been wishing for something like that but have not much energy into it.
I'll at least try to find time to download and try out!
Concerning the minimality of the proof, I think this can still be
achieved later on with the same tool, either by adding a last step
mimicking the metamath program's "minimize" once the proof is known, or
by improving the strategies so that they produce shorter proofs, or both.
I think you call "WFF" is probably a SAT predicate calculus prover, so
maybe that name would fit better?
And then the Z3 prover would be a first-order logic SMT prover.
BR,
_
Thierry
This sounds very promising!
I've been wishing for something like that but have not much energy into it.
I'll at least try to find time to download and try out!
Concerning the minimality of the proof, I think this can still be
achieved later on with the same tool, either by adding a last step
mimicking the metamath program's "minimize" once the proof is known, or
by improving the strategies so that they produce shorter proofs, or both.
I think you call "WFF" is probably a SAT predicate calculus prover, so
maybe that name would fit better?
And then the Z3 prover would be a first-order logic SMT prover.
BR,
_
Thierry
Glauco
Mar 28, 2018, 2:55:28 PM3/28/18
to Metamath
Hi Giovanni,
I've tried to follow the instructions (Ubuntu 16.4)
At the make step, I get some warnings and errors (below I copy till the first couple of errors). Is there any screenshot ( video :-) ) available?
g++ -c -m64 -pipe -g -ftemplate-backtrace-limit=0 -O2 -Wall -W -fPIC -DPROJ_DIR="\"/home/<snip>/mmpp\"" -DUSE_MICROHTTPD -DUSE_Z3 -I../../mmpp -I. -isystem /usr/include/p11-kit-1 -I/usr/lib/x86_64-linux-gnu/qt5/mkspecs/linux-g++-64 -o main.o ../main.cpp
In file included from /usr/include/c++/5/chrono:35:0,
from ../utils/utils.h:14,
from ../main.cpp:8:
/usr/include/c++/5/bits/c++0x_warning.h:32:2: error: #error This file requires compiler and library support for the ISO C++ 2011 standard. This support must be enabled with the -std=c++11 or -std=gnu++11 compiler options.
#error This file requires compiler and library support \
^
In file included from ../main.cpp:8:0:
../utils/utils.h:235:5: warning: identifier ‘constexpr’ is a keyword in C++11 [-Wc++0x-compat]
constexpr SafeWeakPtr() noexcept : std::weak_ptr< T >() {
^
../utils/utils.h:235:5: warning: identifier ‘noexcept’ is a keyword in C++11 [-Wc++0x-compat]
../utils/utils.h:271:1: warning: identifier ‘decltype’ is a keyword in C++11 [-Wc++0x-compat]
auto vector_map(InputIt from, InputIt to, UnaryOperation op) -> std::vector< de
^
../utils/utils.h:64:39: warning: variadic templates only available with -std=c++11 or -std=gnu++11
template< typename Exception, typename... Args >
^
../utils/utils.h:65:62: warning: variadic templates only available with -std=c++11 or -std=gnu++11
inline static void assert_or_throw(bool cond, const Args&... args) {
^
../utils/utils.h:75:10: error: ‘chrono’ in namespace ‘std’ does not name a type
std::chrono::steady_clock::time_point begin;
^
../utils/utils.h:81:24: error: ‘function’ is not a member of ‘std’
std::map< std::string, std::function< int(int, char*[]) > > &get_main_functions
Jim Kingdon
Mar 28, 2018, 4:05:51 PM3/28/18
to Glauco, Metamath
Ubuntu 16.4 requires getting a copy of GCC other than the one which comes with the operating system. The README should now have directions.
More discussion at https://github.com/giomasce/mmpp/issues/1
More discussion at https://github.com/giomasce/mmpp/issues/1
David A. Wheeler
Mar 28, 2018, 8:37:45 PM3/28/18
to Jim Kingdon, Glauco, Metamath
It's a little unfortunate that you have to install a special compiler, instead of the normal one, for the current long-term supported operating system. What are the capabilities that cause this?
--- David A.Wheeler
--- David A.Wheeler
Giovanni Mascellani
Mar 29, 2018, 5:32:49 AM3/29/18
to meta...@googlegroups.com
Hi,
Il 28/03/2018 22:04, Jim Kingdon ha scritto:
> Ubuntu 16.4 requires getting a copy of GCC other than the one which
> comes with the operating system. The README should now have directions.
>
> More discussion at https://github.com/giomasce/mmpp/issues/1
For the benefit of those who are interested in the discussion but do not
follow the GitHub issue, I have implemented a few changes (less than I
expected in the first time), so that now mmpp compile with C++14 and
with GCC 5. So now Ubuntu LTS users should be able to build it without
having to install another compiler.
Please let me know if there are some other blockers.
Il 28/03/2018 22:04, Jim Kingdon ha scritto:
> Ubuntu 16.4 requires getting a copy of GCC other than the one which
> comes with the operating system. The README should now have directions.
>
> More discussion at https://github.com/giomasce/mmpp/issues/1
follow the GitHub issue, I have implemented a few changes (less than I
expected in the first time), so that now mmpp compile with C++14 and
with GCC 5. So now Ubuntu LTS users should be able to build it without
having to install another compiler.
Please let me know if there are some other blockers.
Reply all
Reply to author
Forward
0 new messages