[POC] run Elpi code in lambdapi

[gares]

do not merge this is a POC to be discussed at a seminar on the 18th

TODO (hopefully for the 18th):

• support Terms.Meta in the HOAS encoding using Elpi's unification variables
• from Terms.term Conversion.t to (Terms.term,Env.t,_) ContextualConversion.t
• bind Typing.infer(_constr) and Eval.eq_modulo

[fblanqui]

Ouah. That's great @gares . Thank you for digging into the code of Lambdapi !

[gares]

CI seems to be failing because of "sanity_check" but it does not seem to have much to do with my code (locally it prints messages about files I did not touch). Is it expected?

[fblanqui]

Yes:

18:39 ~/lambdapi (elpi) make sanity_check
In src/core/ctxt.ml, line 12 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 53 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 95 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 99 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 175 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 259 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 263 more than 78 characters...

Please run tools/git_hook_helper.sh to have the following pre-commit hook:

#!/bin/sh
if [ ! -z "$(make sanity_check)" ]; then
    echo "Sanity check failed."
    exit 1
fi

[gares]

I did set it up, but then I could not commit anything. If I run the script locally I get

gares@ollypat:~/work-area/lambdapi$ make sanity_check 
In src/cli/lambdapi.ml, line 30 more than 78 characters...
In src/core/basics.ml, line 30 more than 78 characters...
In src/core/builtin.ml, line 10 more than 78 characters...
... many other files, including mine, ....

here line 30 of src/cli/lambdapi.ml has 79 chars according to my editor.

Anyway, I'll fix my file, I did not spot it in the sea of errors it prints here

[fblanqui]

Well, 79>78 indeed ;-) But that's strange we do not get the same files! Do you use gawk? I have GNU Awk 4.1.4. Could you please give the complete result of make sanity_check too?

[gares]

Well spotted, I've no idea why my ubuntu has this variant of awk (by default)

gares@ollypat:~/work-area/lambdapi$ dpkg -l | grep awk
ii  mawk                                       1.3.3-17ubuntu3                                  amd64        a pattern scanning and text processing language

I've installed gawk, it now works

[gabrielhdt]

It's not the first time it happens, perhaps we should check the awk version with a awk --version | grep GNU or something of the kind...

[fblanqui]

Why not simply calling gawk explicitly instead of awk?

[fblanqui]

tools/git_hook_helper.sh could also check that gawk exists

[fblanqui]

Fixed in f2c363c

[fblanqui]

You can remove the diff here.

[fblanqui]

Missing explanation of the function.

[fblanqui]

Missing explanation of the function.