Compile issue with Basics.v

[tpottei1]

I am having an issue with the compilation of Basics.v. What could be a cause for this error?

make[1]: Entering directory '/home/tpottei1/InteractionTrees' COQC theories/Basics/Basics.v File "./theories/Basics/Basics.v", line 166, characters 15-21: Error: In environment M : Type -> Type S : Type MM : Monad M AM : MonadIter M T : Type T0 : Type step : T0 -> stateT S M (T0 + T) i : T0 s : Type The term "(i, s)" has type "(T0 Type)%type" while it is expected to have type "(T0 S)%type".

Makefile.coq:662: recipe for target 'theories/Basics/Basics.vo' failed make[2]: [theories/Basics/Basics.vo] Error 1 Makefile.coq:326: recipe for target 'all' failed make[1]: [all] Error 2 make[1]: Leaving directory '/home/tpottei1/InteractionTrees' common.mk:6: recipe for target 'coq' failed make: *** [coq] Error 2

[Lysxia]

One likely cause is an incompatible version of coq-ext-lib. Make sure you have coq-ext-lib 0.10.2.

[tpottei1]

Thank you, updating coq-ext-lib 0.10.2 allowed me to get past the issue with Basics.v. But, I am having an issue now with Eq.v not compiling.

make -f Makefile.coq make[1]: Entering directory '/home/tpottei1/InteractionTrees' COQC theories/Eq/Eq.v File "./theories/Eq/Eq.v", line 179, characters 15-20: Error: The reference pstep was not found in the current environment.

Makefile.coq:662: recipe for target 'theories/Eq/Eq.vo' failed make[2]: [theories/Eq/Eq.vo] Error 1 Makefile.coq:326: recipe for target 'all' failed make[1]: [all] Error 2 make[1]: Leaving directory '/home/tpottei1/InteractionTrees' common.mk:6: recipe for target 'coq' failed make: *** [coq] Error 2

Is this error a result of using an incompatible version of paco?

[YaZko]

Indeed failing to find pstep suggests an outdated version of paco. You should have the version 4.0.0 installed. Best, Yannick

[tpottei1]

Thank you for the quick response. Using coq-paco.4.0.0 and coq-ext-lib.0.10.2, I am able to compile successfully.