bmake check does not seem to work properly

[fblanqui]

bmake check ends instantaneously: it does seem to do anything.
Moreover, nubo seems to use dkcheck instead of dk check.

[gabrielhdt]

In which directory did you run bmake check?

[gabrielhdt]

For the dkcheck v dk check, indeed you're right, it can be seen there

nubo/infrastructure/mk/dedukti.mk

Line 1 in 6d81cd8

CHECK ?= dkcheck 2> /dev/null

Probably we'd like the program to check the version of the tools that are used (for better reproducibility).

[fblanqui]

19:21 ~/src/nubo/libraries/arith_fermat/sttfa,1.0 (master) bmake download
===> Downloading
######################################################################### 100,0%
OK
===> Unpacking
OK
19:21 ~/src/nubo/libraries/arith_fermat/sttfa,1.0 (master) time bmake check
===> Proof checking
OK

real	0m0,404s
user	0m0,354s
sys	0m0,050s
19:21 ~/src/nubo/libraries/arith_fermat/sttfa,1.0 (master) ls
arith_fermat-1.0-sttfa/  arith_fermat-1.0-sttfa.tgz  Makefile
19:21 ~/src/nubo/libraries/arith_fermat/sttfa,1.0 (master) ls arith_fermat-1.0-sttfa
bigops.dk  connectives.dk  fact.dk    leibniz.dk  permutation.dk  sigma_pi.dk
bool.dk    div_mod.dk      fermat.dk  logic.dk    primes.dk
cong.dk    exp.dk          gcd.dk     nat.dk      relations.dk

There is no dko files.

[gabrielhdt]

IIRC, dko files are stored in the cache directory, which ought to be the directory _cache. This is defined at

nubo/infrastructure/mk/nubo.library.mk

Line 25 in 6d81cd8

CACHE ?= ${NUBOROOT}/_cache

So normally, the dkos should be in ~/src/nubo/_cache (what does find ~/src/nubo/_cache -name '*.dko' say?)

[fblanqui]

I see. Thank you Gabriel. Could you please document this and update the dk checker name?
I am also wondering if it wouldn't be better to be more verbose on what's happening, for instance by printing the names of checked files?