Cannot build Logipedia

[rprimet]

With the last published version of Deduki, a build of Logipedia fails. It seems to pass when building Dedukti from the Github master head though; maybe this should be added to the README (as well as with instructions on building the Dedukti master head through opam?)

(also, the suggestion to run make main to build the project fails)

Apologies if I missed something, I am unfamiliar with Ocaml.

romain@plume:~/inria/logipedia/Logipedia$ opam list
# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
bson                0.89.3      A bson data structure, including encoding/decodi
conf-m4             1           Virtual package relying on m4
dedukti             2.6.0       The Dedukti logical framework
menhir              20181113    An LR(1) parser generator
mongo               0.67.2      OCaml driver for MongoDB
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlbuild          0.14.0      OCamlbuild is a build system with builtin rules 
ocamlfind           1.8.0       A library manager for OCaml

romain@plume:~/inria/logipedia/Logipedia$ git status
Sur la branche master
Votre branche est à jour avec 'origin/master'.

rien à valider, la copie de travail est propre

romain@plume:~/inria/logipedia/Logipedia$ make clean && make
[DEP] .library_depend_lean
[DEP] .library_depend_art
[DEP] .library_depend_ma
[DEP] .library_depend_v
[DEP] .library_depend_vo
[DEP] .library_depend_pvs
[DEP] .library_depend_dko
[BUILD] main.native
+ ocamlfind ocamlc -c -thread -package dedukti -package mongo -I src -I src/utils -I src/export -o src/decompile.cmo src/decompile.ml
File "src/decompile.ml", line 80, characters 4-16:
Error: Unbound value Term.mk_App2
Hint: Did you mean mk_App?
Command exited with code 2.
Hint: Recursive traversal of subdirectories was not enabled for this build,
  as the working directory does not look like an ocamlbuild project (no
  '_tags' or 'myocamlbuild.ml' file). If you have modules in subdirectories,
  you should add the option "-r" or create an empty '_tags' file.

  To enable recursive traversal for some subdirectories only, you can use the
  following '_tags' file:

      true: -traverse
      <dir1> or <dir2>: traverse

GNUmakefile:12: recipe for target '_build/src/main.native' failed
make: *** [_build/src/main.native] Error 10
romain@plume:~/inria/logipedia/Logipedia$ 

[francoisthire]

Indead, you need tha last version of Dedukti on the master branch.

The easiest way (at least for me) is to run (for Dedukti) make install

which will install the files in the opam repository.

Then, you can build Logipedia. I know that there is another way with opam pin, but I am not very familiar with: https://opam.ocaml.org/doc/Usage.html#opam-pin

[rprimet]

Thanks!