ml4tp / tcoq Goto Github PK

What does:

3- The uncompression and un-tarring of the distribution file gave birth
to a directory named "coq-8.xx". You can rename this directory and put
it wherever you want. Just keep in mind that you will need some spare
space during the compilation (reckon on about 300 Mb of disk space
for the whole system in native-code compilation). Once installed, the
binaries take about 30 Mb, and the library about 200 Mb.

mean and how does one do this?

I wanted to see what sort of information it dumped out.

is inserting:

export tcoq="/Users/me/gamepad/tcoq/bin/coqc"

enough? I see there are many other files in the bin directory...am I missing anything else?

specifically:

#!/usr/bin/env bash

echo "Configuring Coq..."
make clean
mkdir build
./configure -prefix build

what is the advantages/disadvantages and difference between using SerAPI vs TCoq?

https://github.com/ejgallego/coq-serapi