Deducteam/Holide

configure: dkcheck called with wrong option

fblanqui opened this issue · 1 comments

Hi. Following README.md, we just have to do make. But I get the following error on my machine:

07:03 ~/src/Holide (master) make
classic-display -libs str -I src -build-dir build main.native
bash: classic-display : commande introuvable
make: [Makefile:73 : holide] Erreur 127 (ignorée)
ln -sf build/src/main.native holide
cd dedukti/ && "/home/blanqui/.opam/4.11.1/bin/dkcheck" -e hol.dk
[SUCCESS] hol.dk was successfully checked.

Now, ./configure fails as well:

07:03 ~/src/Holide (master) ./configure 
Looking for program 'dkcheck' in PATH.
Program 'dkcheck' found in PATH at "/home/blanqui/.opam/4.11.1/bin/dkcheck".
Asking 'dkcheck' for its version number.
Program 'dkcheck' has version '[Warning] [DEPRECATED] Flag -version is deprecated ! Use --version instead.

devel'.
./configure: ligne 22 : [: 2.6 : opérateur unaire attendu

ERROR: version constraint not satisfied: 2.6 <= [Warning] [DEPRECATED] Flag -version is deprecated ! Use --version instead.

devel

ERROR: version constraint not satisfied: [Warning] [DEPRECATED] Flag -version is deprecated ! Use --version instead.

devel = devel

The problem is that, to get the version of dkcheck, we need to use --version now, instead of -version before. After that, everything works.