issues installing

[brando90]

the instructions are a bit unclear. I real ./get_data.sh then I did ./setup_tcoq.sh but I get error:

./setup_tcoq.sh
~/home_simulation_research/gamepad/tcoq ~/home_simulation_research/gamepad
Configuring Coq...
make: *** No rule to make target `clean'.  Stop.
mkdir: build: File exists
./setup_tcoq.sh: line 7: ./configure: No such file or directory
~/home_simulation_research/gamepad

what is configure and how do we get it?

[spolu]

You probably want to run get_data.sh such that the tcoq submodule gets init/updated first.

[brando90]

I had already done that:

$ ./get_data.sh 'tcoq' already exists in the index fatal: destination path '/Users/brandomiranda/home_simulation_research/gamepad/tcoq' already exists and is not an empty directory. fatal: clone of 'https://github.com/ml4tp/tcoq.git' into submodule path '/Users/brandomiranda/home_simulation_research/gamepad/tcoq' failed Failed to clone 'tcoq'. Retry scheduled fatal: destination path '/Users/brandomiranda/home_simulation_research/gamepad/tcoq' already exists and is not an empty directory. fatal: clone of 'https://github.com/ml4tp/tcoq.git' into submodule path '/Users/brandomiranda/home_simulation_research/gamepad/tcoq' failed Failed to clone 'tcoq' a second time, aborting fatal: destination path 'math-comp' already exists and is not an empty directory. ~/home_simulation_research/gamepad/math-comp ~/home_simulation_research/gamepad HEAD is now at b4510cb back port bug fixes and plugin porting to Coq 8.6 from master ~/home_simulation_research/gamepad fatal: destination path 'odd-order' already exists and is not an empty directory. ~/home_simulation_research/gamepad/odd-order ~/home_simulation_research/gamepad HEAD is now at f1f066e finfield ~/home_simulation_research/gamepad

[brando90]

@spolu what I am confused about is how to deal with the 2nd instruction:

Configure tcoq. ./setup_tcoq.sh

I've looked at that script but its really simple set of commands with:

#!/usr/bin/env bash

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

and there is no makefile or any ./configure file...

[brando90]

does the error mean the makefile is missing?

https://stackoverflow.com/questions/4182118/make-clean-results-in-no-rule-to-make-target-clean

[brando90]

after the opam comands

Run 
git submodule update --init
After that completes run:
./get_data.sh

then continue from step 2