giomasce / mmpp Goto Github PK
View Code? Open in Web Editor NEWMetamath in C++
Metamath in C++
When I build on Ubuntu 16.04 using the instructions in the README, I get:
../mm/tokenizer.h:35:24: error: ‘ifstream’ in namespace ‘boost::filesystem’ does not name a type
The version of boost from dpkg -l | grep boost-all-dev
is 1.58.0.1ubuntu1
.
Building commit c964d72 fails on provers/subst.cpp
Lines 30 to 63 in c964d72
on Ubuntu 16.04 LTS using gcc/g++ (Ubuntu 5.4.0-6ubuntu1~16.04.9) 5.4.0 20160609
, with the following build error:
> make
g++ -c -m64 -pipe -g -ftemplate-backtrace-limit=0 -Og -std=c++1y -Wall -W -fPIC -DPROJ_DIR="\"/home/marnix/projects/mmpp\"" -DDISABLE_TESTS -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 subst.o ../provers/subst.cpp
../provers/subst.cpp:63:1: error: converting to ‘std::tuple<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::vector<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > > >’ from initializer list would use explicit constructor ‘constexpr std::tuple< <template-parameter-1-1> >::tuple(const _Elements& ...) [with _Elements = {std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::vector<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > >}]’
};
^
I have no idea yet what could be the cause, except that perhaps https://stackoverflow.com/q/26947704/223837 might be related.
The addition of boost::unit_test::data, for xrange (see diff 673f7de#diff-041c9b3c31d7bf42b4e96a5bf35622dfR11) broke the build on Ubuntu 16.04:
g++ -c -m64 -pipe -g -ftemplate-backtrace-limit=0 -Og -std=c++1y -Wall -W -fPIC -DPROJ_DIR="\"/home/marnix/projects/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 unification.o ../old/unification.cpp
In file included from ../old/unification.cpp:10:0:
../../mmpp/test/test.h:12:61: fatal error: boost/test/data/monomorphic/generators/xrange.hpp: No such file or directory
compilation terminated.
Makefile:614: recipe for target 'unification.o' failed
make: *** [unification.o] Error 1
At least my system has packages libboost-test1.58-dev and libboost-test1.58.0 for boost::unit_test.
And boost::unit_test::data was added in 1.59, it looks like. (I deduce that from the phrase "data driven test cases" under the 'Boost.Test v3' heading in the Boost 1.59 release notes, together with the 1.59.0 documentation.)
Hello everyone, I am using macOS Catalina 10.15.7. I have followed the installation instructions given in the README and I got this error during the build.
../mm/toolbox.cpp:1233:53: error: no member named '__cxx11' in namespace 'std'
Prover<ProofEngine> make_throwing_prover(const std::__cxx11::string &msg) {
Here is the full build output log,
https://gist.github.com/hiiroo/4a03f7bdba7f2a2b692c3b1d54b2caec
Thanks
Ubuntu 16.04 is the most recent LTS release for Ubuntu.
When I follow the instructions in the README, I get the following error in the make
step:
g++ -c -m64 -pipe -g -ftemplate-backtrace-limit=0 -O2 -Wall -W -fPIC -DPROJ_DIR="\"/home/jkingdon/work/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 \
^
There are more errors after that point but perhaps that makes the point. Editing the makefile with -std=c++17
gets slightly farther but only slightly.
Running g++ -v
shows gcc version 5.4.0 20160609 (Ubuntu 5.4.0-6ubuntu1~16.04.9)
If the answer is a newer GCC, perhaps the directions should point to ppa:jonathonf/gcc-7.1
as shown at
https://askubuntu.com/questions/1008744/when-will-gcc-be-updated-in-16-04-and-18-04/1008746
For myself, I suppose I'll just wait for 18.04 although I guess it will be several months before that is a recommended upgrade from 16.04.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.