Skip to content

pmGenerator 1.2 (patch 2)

Latest
Latest

Choose a tag to compare

View all tags
@xamidi xamidi released this 07 Jun 17:20
· 10 commits to master since this release
1.2.2
402311a

pmGenerator-1.2.2-win.7z contains Windows binaries only.

Known issues and workarounds

  • The Windows Command Prompt (CMD) does not support UTF-8 encoded output, e.g. ≈ is printed as Ôëê. [won't fix]
    • You can work around this by redirecting all output into a file like pmGenerator [args] > out.txt 2>&1,
      or by using a different console, e.g. Cygwin64 Terminal that comes with Cygwin (and requires Unix notation, like ./pmGenerator).
    • The command chcp 65001 after configuring cmd.exe to use an appropriate font (such as "Consolas" or "Lucida Console") temporarily enables UTF-8 for CMD on newer Windows versions (such as Windows 10). However, on older versions (such as Windows 7), this may lead to incorrect behavior — like cutting off the output — due to insufficient support of required features.
      • You can make UTF-8 settings permanent for cmd.exe by creating or modifying the AutoRun registry entry of type "String Value" (REG_SZ) under HKEY_LOCAL_MACHINE\Software\Microsoft\Command Processor (all users) or HKEY_CURRENT_USER\Software\Microsoft\Command Processor (current user only) to chcp 65001.
        For example, via executing the following Windows Registration Entries (.reg) file: 
        Windows Registry Editor Version 5.00
[HKEY_CURRENT_USER\SOFTWARE\Microsoft\Command Processor]
"AutoRun"="chcp 65001"

Exemplary build scripts

Linux

  • Exemplary compiler options -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread
  • Exemplary linker options -pthread -ltbb
build.sh 
#!/bin/zsh
cmp='-O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread'
inc='-I/home/oneTBB/include/'
lnk='-pthread -ltbb'
lib='-L/home/oneTBB/intel_19.0_cxx11_64_relwithdebinfo/'
mkdir -p {helper,cryptography,grammar,metamath,nd,logic}
set -x
export I_MPI_CXX=icpx
mpicxx $inc $cmp -o helper/FctHelper.o ../helper/FctHelper.cpp
mpicxx $inc $cmp -o helper/IPrintable.o ../helper/IPrintable.cpp
mpicxx $inc $cmp -o helper/ProgressData.o ../helper/ProgressData.cpp
mpicxx $inc $cmp -o helper/Resources.o ../helper/Resources.cpp
mpicxx $inc $cmp -o cryptography/sha2.o ../cryptography/sha2.cpp
mpicxx $inc $cmp -o grammar/CfgGrammar.o ../grammar/CfgGrammar.cpp
mpicxx $inc $cmp -o grammar/CfgParser.o ../grammar/CfgParser.cpp
mpicxx $inc $cmp -o metamath/DRuleParser.o ../metamath/DRuleParser.cpp
mpicxx $inc $cmp -o metamath/DRuleReducer.o ../metamath/DRuleReducer.cpp
mpicxx $inc $cmp -o nd/NdConverter.o ../nd/NdConverter.cpp
mpicxx $inc $cmp -o nd/NdParser.o ../nd/NdParser.cpp
mpicxx $inc $cmp -o logic/DlCore.o ../logic/DlCore.cpp
mpicxx $inc $cmp -o logic/DlFormula.o ../logic/DlFormula.cpp
mpicxx $inc $cmp -o logic/DlProofEnumerator.o ../logic/DlProofEnumerator.cpp
mpicxx $inc $cmp -o logic/DlStructure.o ../logic/DlStructure.cpp
mpicxx $inc $cmp -o main.o ../main.cpp
mpicxx $lib $lnk -o pmGenerator cryptography/sha2.o grammar/CfgGrammar.o grammar/CfgParser.o helper/FctHelper.o helper/IPrintable.o helper/ProgressData.o helper/Resources.o main.o metamath/DRuleParser.o metamath/DRuleReducer.o nd/NdConverter.o nd/NdParser.o logic/DlCore.o logic/DlFormula.o logic/DlProofEnumerator.o logic/DlStructure.o
clean.sh 
#!/bin/zsh
rm {helper,cryptography,grammar,metamath,nd,logic} -r
rm main.o
rm pmGenerator
compile.sh 
#!/bin/zsh
cmp='-O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread'
inc='-I/home/oneTBB/include/'
mkdir -p {helper,cryptography,grammar,metamath,nd,logic}
set -x
export I_MPI_CXX=icpx
mpicxx $inc $cmp -o helper/FctHelper.o ../helper/FctHelper.cpp
mpicxx $inc $cmp -o helper/IPrintable.o ../helper/IPrintable.cpp
mpicxx $inc $cmp -o helper/ProgressData.o ../helper/ProgressData.cpp
mpicxx $inc $cmp -o helper/Resources.o ../helper/Resources.cpp
mpicxx $inc $cmp -o cryptography/sha2.o ../cryptography/sha2.cpp
mpicxx $inc $cmp -o grammar/CfgGrammar.o ../grammar/CfgGrammar.cpp
mpicxx $inc $cmp -o grammar/CfgParser.o ../grammar/CfgParser.cpp
mpicxx $inc $cmp -o metamath/DRuleParser.o ../metamath/DRuleParser.cpp
mpicxx $inc $cmp -o metamath/DRuleReducer.o ../metamath/DRuleReducer.cpp
mpicxx $inc $cmp -o nd/NdConverter.o ../nd/NdConverter.cpp
mpicxx $inc $cmp -o nd/NdParser.o ../nd/NdParser.cpp
mpicxx $inc $cmp -o logic/DlCore.o ../logic/DlCore.cpp
mpicxx $inc $cmp -o logic/DlFormula.o ../logic/DlFormula.cpp
mpicxx $inc $cmp -o logic/DlProofEnumerator.o ../logic/DlProofEnumerator.cpp
mpicxx $inc $cmp -o logic/DlStructure.o ../logic/DlStructure.cpp
mpicxx $inc $cmp -o main.o ../main.cpp
link.sh 
#!/bin/zsh
lnk='-pthread -ltbb'
lib='-L/home/oneTBB/intel_19.0_cxx11_64_relwithdebinfo/'
set -x
export I_MPI_CXX=icpx
mpicxx $lib $lnk -o pmGenerator cryptography/sha2.o grammar/CfgGrammar.o grammar/CfgParser.o helper/FctHelper.o helper/IPrintable.o helper/ProgressData.o helper/Resources.o main.o metamath/DRuleParser.o metamath/DRuleReducer.o nd/NdConverter.o nd/NdParser.o logic/DlCore.o logic/DlFormula.o logic/DlProofEnumerator.o logic/DlStructure.o

Windows

build.bat 
SET LIBS_HOME=C:/Users/%USERNAME%/Dropbox/eclipse
SET GCC_HOME=D:/winlibs-x86_64-posix-seh-gcc-11.3.0-llvm-14.0.3-mingw-w64msvcrt-10.0.0-r3/mingw64
SET gcc=%GCC_HOME%/bin/g++
SET cmp=-O3 -fno-align-functions -fno-align-jumps -fno-align-loops -fno-align-labels -pedantic -Wall -Wconversion -c -m64 -fmessage-length=0 -std=c++20 -D_FILE_OFFSET_BITS=64
SET inc=-I%LIBS_HOME%/boost_1_88_0/include -I%LIBS_HOME%/mingw-w64-x86_64-msmpi-10.1.1-10-any.pkg/mingw64/include -I%LIBS_HOME%/mingw-w64-x86_64-tbb-2021.9.0-1-any.pkg/mingw64/include
SET lnk=-s -Wl,--subsystem,console -fuse-ld=lld -lpthread -ltbb12.dll -lmsmpi.dll
SET lib=-L%LIBS_HOME%/mingw-w64-x86_64-tbb-2021.9.0-1-any.pkg/mingw64/lib -L%LIBS_HOME%/mingw-w64-x86_64-msmpi-10.1.1-10-any.pkg/mingw64/lib
for %%s in (helper cryptography grammar metamath nd logic) do if not exist %%s ( mkdir %%s )
%gcc% %inc% %cmp% -o helper\FctHelper.o ..\helper\FctHelper.cpp
%gcc% %inc% %cmp% -o helper\IPrintable.o ..\helper\IPrintable.cpp
%gcc% %inc% %cmp% -o helper\ProgressData.o ..\helper\ProgressData.cpp
%gcc% %inc% %cmp% -o helper\Resources.o ..\helper\Resources.cpp
%gcc% %inc% %cmp% -o cryptography\sha2.o ..\cryptography\sha2.cpp
%gcc% %inc% %cmp% -o grammar\CfgGrammar.o ..\grammar\CfgGrammar.cpp
%gcc% %inc% %cmp% -o grammar\CfgParser.o ..\grammar\CfgParser.cpp
%gcc% %inc% %cmp% -o metamath\DRuleParser.o ..\metamath\DRuleParser.cpp
%gcc% %inc% %cmp% -o metamath\DRuleReducer.o ..\metamath\DRuleReducer.cpp
%gcc% %inc% %cmp% -o nd\NdConverter.o ..\nd\NdConverter.cpp
%gcc% %inc% %cmp% -o nd\NdParser.o ..\nd\NdParser.cpp
%gcc% %inc% %cmp% -o logic\DlCore.o ..\logic\DlCore.cpp
%gcc% %inc% %cmp% -o logic\DlFormula.o ..\logic\DlFormula.cpp
%gcc% %inc% %cmp% -o logic\DlProofEnumerator.o ..\logic\DlProofEnumerator.cpp
%gcc% %inc% %cmp% -o logic\DlStructure.o ..\logic\DlStructure.cpp
%gcc% %inc% %cmp% -o main.o ..\main.cpp

:: Required for -fuse-ld=lld
set PATH=%PATH%;%GCC_HOME%/bin

%GCC_HOME%/bin/windres ../icon/icon.rc -O coff -o icon.o --use-temp-file
%gcc% -o pmGenerator.exe icon.o cryptography/sha2.o grammar/CfgGrammar.o grammar/CfgParser.o helper/FctHelper.o helper/IPrintable.o helper/ProgressData.o helper/Resources.o main.o metamath/DRuleParser.o metamath/DRuleReducer.o nd/NdConverter.o nd/NdParser.o logic/DlCore.o logic/DlFormula.o logic/DlProofEnumerator.o logic/DlStructure.o %lnk% %lib%

@echo off
pause
clean.bat 
@echo off
for %%s in (helper cryptography grammar metamath nd logic) do if exist %%s ( del /S %%s\*.o )

@echo on
del icon.o
del main.o
del pmGenerator.exe

@echo off
pause
compile.bat 
SET LIBS_HOME=C:/Users/%USERNAME%/Dropbox/eclipse
SET GCC_HOME=D:/winlibs-x86_64-posix-seh-gcc-11.3.0-llvm-14.0.3-mingw-w64msvcrt-10.0.0-r3/mingw64
SET gcc=%GCC_HOME%/bin/g++
SET cmp=-O3 -fno-align-functions -fno-align-jumps -fno-align-loops -fno-align-labels -pedantic -Wall -Wconversion -c -m64 -fmessage-length=0 -std=c++20 -D_FILE_OFFSET_BITS=64
SET inc=-I%LIBS_HOME%/boost_1_88_0/include -I%LIBS_HOME%/mingw-w64-x86_64-msmpi-10.1.1-10-any.pkg/mingw64/include -I%LIBS_HOME%/mingw-w64-x86_64-tbb-2021.9.0-1-any.pkg/mingw64/include
for %%s in (helper cryptography grammar metamath nd logic) do if not exist %%s ( mkdir %%s )
%gcc% %inc% %cmp% -o helper\FctHelper.o ..\helper\FctHelper.cpp
%gcc% %inc% %cmp% -o helper\IPrintable.o ..\helper\IPrintable.cpp
%gcc% %inc% %cmp% -o helper\ProgressData.o ..\helper\ProgressData.cpp
%gcc% %inc% %cmp% -o helper\Resources.o ..\helper\Resources.cpp
%gcc% %inc% %cmp% -o cryptography\sha2.o ..\cryptography\sha2.cpp
%gcc% %inc% %cmp% -o grammar\CfgGrammar.o ..\grammar\CfgGrammar.cpp
%gcc% %inc% %cmp% -o grammar\CfgParser.o ..\grammar\CfgParser.cpp
%gcc% %inc% %cmp% -o metamath\DRuleParser.o ..\metamath\DRuleParser.cpp
%gcc% %inc% %cmp% -o metamath\DRuleReducer.o ..\metamath\DRuleReducer.cpp
%gcc% %inc% %cmp% -o nd\NdConverter.o ..\nd\NdConverter.cpp
%gcc% %inc% %cmp% -o nd\NdParser.o ..\nd\NdParser.cpp
%gcc% %inc% %cmp% -o logic\DlCore.o ..\logic\DlCore.cpp
%gcc% %inc% %cmp% -o logic\DlFormula.o ..\logic\DlFormula.cpp
%gcc% %inc% %cmp% -o logic\DlProofEnumerator.o ..\logic\DlProofEnumerator.cpp
%gcc% %inc% %cmp% -o logic\DlStructure.o ..\logic\DlStructure.cpp
%gcc% %inc% %cmp% -o main.o ..\main.cpp

@echo off
pause
link.bat 
SET LIBS_HOME=C:/Users/%USERNAME%/Dropbox/eclipse
SET GCC_HOME=D:/winlibs-x86_64-posix-seh-gcc-11.3.0-llvm-14.0.3-mingw-w64msvcrt-10.0.0-r3/mingw64
SET gcc=%GCC_HOME%/bin/g++
SET lnk=-s -Wl,--subsystem,console -fuse-ld=lld -lpthread -ltbb12.dll -lmsmpi.dll
SET lib=-L%LIBS_HOME%/mingw-w64-x86_64-tbb-2021.9.0-1-any.pkg/mingw64/lib -L%LIBS_HOME%/mingw-w64-x86_64-msmpi-10.1.1-10-any.pkg/mingw64/lib

:: Required for -fuse-ld=lld
set PATH=%PATH%;%GCC_HOME%/bin

%GCC_HOME%/bin/windres ../icon/icon.rc -O coff -o icon.o --use-temp-file
%gcc% -o pmGenerator.exe icon.o cryptography/sha2.o grammar/CfgGrammar.o grammar/CfgParser.o helper/FctHelper.o helper/IPrintable.o helper/ProgressData.o helper/Resources.o main.o metamath/DRuleParser.o metamath/DRuleReducer.o nd/NdConverter.o nd/NdParser.o logic/DlCore.o logic/DlFormula.o logic/DlProofEnumerator.o logic/DlStructure.o %lnk% %lib%

@echo off
pause

Verified to compile with GCC, Clang/LLVM, and MSVC.

Assets 7
Loading