giomasce / mmpp Goto Github PK

Metamath in C++

C++ 93.64% QMake 0.43% HTML 0.03% TypeScript 3.96% CSS 0.13% JavaScript 1.11% C 0.10% Dockerfile 0.06% Scala 0.52% Shell 0.02%

mmpp's People

Contributors

Stargazers

Watchers

Forkers

marnix pyzh

mmpp's Issues

macOS Catalina error: no member named '__cxx11' in namespace 'std'

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

Installation does not succeed on Ubuntu 16.04

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.

‘ifstream’ in namespace ‘boost::filesystem’ does not name a type

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 .

Ubuntu 16.04 has Boost 1.58, but the required boost::unit_test::data is part of Boost >= 1.59

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.)

provers/subst.cpp build error with gcc/g++ 5.4.0 on Ubuntu 16.04 LTS

Building commit c964d72 fails on provers/subst.cpp

mmpp/provers/subst.cpp

Lines 30 to 63 in c964d72

 std::vector< std::tuple< std::string, std::string, std::vector< std::pair< std::string, std::string > > > > raw_bound_data = { 

 { "class { x | ph }", "ph", { { "x", "" } } }, 

 { "class { x e. A | ph }", "ph", { { "x", "A" } } }, 

 { "class [_ A / x ]_ B", "B", { { "x", "" } } }, 

 { "class U_ x e. A B", "B", { { "x", "A" } } }, 

 { "class |^|_ x e. A B", "B", { { "x", "A" } } }, 

 { "class { <. x , y >. | ph }", "ph", { { "x", "" }, { "y", "" } } }, 

 { "class ( x e. A |-> B )", "B", { { "x", "A" } } }, 

 { "class ( iota x ph )", "ph", { { "x", "" } } }, 

 { "class { <. <. x , y >. , z >. | ph }", "ph", { { "x", "" }, { "y", "" }, { "z", "" } } }, 

 { "class ( x e. A , y e. B |-> C )", "C", { { "x", "A" }, { "y", "B" } } }, 

 { "class ( iota_ x e. A ph )", "ph", { { "x", "" } } }, 

 { "class X_ x e. A B", "B", { { "x", "A" } } }, 

 { "class sum_ x e. A B", "B", { { "x", "A" } } }, 

 { "class S. A B _d x", "B", { { "x", "A" } } }, 

 { "class S_ [ A -> B ] C _d x", "C", { { "x", "" } } }, // Might be relaxed 

 { "class sum* x e. A B", "B", { { "x", "A" } } }, 

 { "class prod_ x e. A B", "B", { { "x", "A" } } }, 

 { "wff A. x ph", "ph", { { "x", "" } } }, 

 { "wff E. x ph", "ph", { { "x", "" } } }, 

 { "wff F/ x ph", "ph", { { "x", "" } } }, 

 { "wff [ x / y ] ph", "ph", { { "y", "" } } }, 

 { "wff E! x ph", "ph", { { "x", "" } } }, 

 { "wff E* x ph", "ph", { { "x", "" } } }, 

 { "wff F/_ x A", "A", { { "x", "" } } }, 

 { "wff A. x e. A ph", "ph", { { "x", "A" } } }, 

 { "wff E. x e. A ph", "ph", { { "x", "A" } } }, 

 { "wff E! x e. A ph", "ph", { { "x", "A" } } }, 

 { "wff E* x e. A ph", "ph", { { "x", "A" } } }, 

 // CondEq?? 

 { "wff [. A / x ]. ph", "ph", { { "x", "" } } }, 

 { "wff Disj_ x e. A B", "B", { { "x", "A" } } }, 

 };

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.

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.

	std::vector< std::tuple< std::string, std::string, std::vector< std::pair< std::string, std::string > > > > raw_bound_data = {
	{ "class { x \| ph }", "ph", { { "x", "" } } },
	{ "class { x e. A \| ph }", "ph", { { "x", "A" } } },
	{ "class [_ A / x ]_ B", "B", { { "x", "" } } },
	{ "class U_ x e. A B", "B", { { "x", "A" } } },
	{ "class \|^\|_ x e. A B", "B", { { "x", "A" } } },
	{ "class { <. x , y >. \| ph }", "ph", { { "x", "" }, { "y", "" } } },
	{ "class ( x e. A \|-> B )", "B", { { "x", "A" } } },
	{ "class ( iota x ph )", "ph", { { "x", "" } } },
	{ "class { <. <. x , y >. , z >. \| ph }", "ph", { { "x", "" }, { "y", "" }, { "z", "" } } },
	{ "class ( x e. A , y e. B \|-> C )", "C", { { "x", "A" }, { "y", "B" } } },
	{ "class ( iota_ x e. A ph )", "ph", { { "x", "" } } },
	{ "class X_ x e. A B", "B", { { "x", "A" } } },
	{ "class sum_ x e. A B", "B", { { "x", "A" } } },
	{ "class S. A B _d x", "B", { { "x", "A" } } },
	{ "class S_ [ A -> B ] C _d x", "C", { { "x", "" } } }, // Might be relaxed
	{ "class sum* x e. A B", "B", { { "x", "A" } } },
	{ "class prod_ x e. A B", "B", { { "x", "A" } } },

	{ "wff A. x ph", "ph", { { "x", "" } } },
	{ "wff E. x ph", "ph", { { "x", "" } } },
	{ "wff F/ x ph", "ph", { { "x", "" } } },
	{ "wff [ x / y ] ph", "ph", { { "y", "" } } },
	{ "wff E! x ph", "ph", { { "x", "" } } },
	{ "wff E* x ph", "ph", { { "x", "" } } },
	{ "wff F/_ x A", "A", { { "x", "" } } },
	{ "wff A. x e. A ph", "ph", { { "x", "A" } } },
	{ "wff E. x e. A ph", "ph", { { "x", "A" } } },
	{ "wff E! x e. A ph", "ph", { { "x", "A" } } },
	{ "wff E* x e. A ph", "ph", { { "x", "A" } } },
	// CondEq??
	{ "wff [. A / x ]. ph", "ph", { { "x", "" } } },
	{ "wff Disj_ x e. A B", "B", { { "x", "A" } } },
	};