lukaszcz/pascaladt

A library of algorithms and data structures for the Free Pascal Compiler.

• CoqHammer: An automated reasoning hammer tool for Coq - proof automation for dependent type theory.

• Coinduction: A Coq plugin to help with proofs by coinduction.

• HCPL: A prototypical proof checker and programming language based on illative combinatory logic.

• Javalette: An educational compiler for Javalette, written in C.

• CMakefile: Automatic build system for C and C++.

• COQ-IMP: Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL".

• CLC: Confluence of an Extension of Combinatory Logic by Boolean Constants: a formalisation of the solution to the RTA open problem 15.

• infinitary-confluence: Formalisation of a coinductive confluence proof for the infinitary lambda calculus.

• sortalgs: Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.

• BST: Binary Search Trees in Coq.

• Diaconescu: Formalisation of two variants of Diaconescu's theorem.

• tptp2coq: Conversion of the FOF TPTP format to Coq files.

• tptp2ileancop: Run ileancop on the ILTP library.

pascaladt's Issues

make fails.

I cannot get the package to build. After downloading and extracting to build by:

tar xcf pascaladt-1.0.2.tar.gz
cd pascaladt-1.0.2
make

the tools directory is built with hashtable/ , mkdeps, mktempl and mcp.

In the main directory the first few files are built, but the make fails with the message

mcp: Fatal error: Cannot open file: adtutils.mcp\n; No such file or directory"

The file adtutils.mcp exists, with permissions:

-rw-r--r-- 1 lucy users 487 Aug 6 18:30 adtutils.mcp

That's the end of the make.

System: SuSE linux, fully patched, identifies as:
uname -a
Linux localhost.localdomain 5.14.21-150500.55.52-default #1 SMP PREEMPT_DYNAMIC Tue Mar 5 16:53:41 UTC 2024 (a62851f) x86_64 x86_64 x86_64 GNU/Linux

Normally make runs with -j 4; the same failure occurs with -j 1.

I will attach a complete log of the attempted build.
make_log.txt

Thanks for your help

deps.mak: No such file or directory

steps:

ADT_VERSION=1.0.1
cd ~/Downloads
wget https://codeload.github.com/lukaszcz/pascaladt/tar.gz/refs/tags/v$ADT_VERSION -O pascaladt-$ADT_VERSION.tar.gz
tar xvf pascaladt-$ADT_VERSION.tar.gz
sudo rm -rf pascaladt-$ADT_VERSION.tar.gz
cd pascaladt-$ADT_VERSION
make

logs:

make[1]: Entering directory '/home/khism/Downloads/pascaladt-1.0.1/tools'
cc -o mktempl mktempl.c
make[1]: cc: No such file or directory
make[1]: *** [Makefile:11: mktempl] Error 127
make[1]: Leaving directory '/home/khism/Downloads/pascaladt-1.0.1/tools'
Makefile:180: deps.mak: No such file or directory
make: *** [Makefile:149: tools.dep] Error 2

Invalid option -M

steps:

ADT_VERSION=1.0.1
cd ~/Downloads
wget https://codeload.github.com/lukaszcz/pascaladt/tar.gz/refs/tags/v$ADT_VERSION -O pascaladt-$ADT_VERSION.tar.gz
tar xvf pascaladt-$ADT_VERSION.tar.gz
sudo rm -rf pascaladt-$ADT_VERSION.tar.gz
cd pascaladt-$ADT_VERSION
make
sudo make install

error (when installing):

make dynamic RELEASE=true OPTS= VER=-1.0.1 MCP_OPTS=-dMCP_REAL -dMCP_CARDINAL -dMCP_POINTER
make: invalid option -- 'M'