Changes since December

[krpcannon]

What's the status of CIC kernel? It seems broken w.r.t. a test written for an older version which was forked shortly after Dalefest in December.

For instance, I see pts_cic accumulated in the alt_0/CIC kernel, but there is no such file in the repo. Minor thing since there are other CiC files in that folder.

But also, I get an error:

Fatal error: Variable can only be introspected (eg ?? X L) in the guard

...when running my test after accumulating:

loading pervasives-syntax.elpi
loading pervasives.elpi
loading kernel_v2.elpi
loading logic.mod
loading list.mod
loading elpi/bench/sources/cic/alt_0/pts_cic_floating.mod
loading elpi/bench/sources/cic/alt_0/refiner_pts.mod
loading elpi/bench/sources/cic/alt_0/kernel_pts.mod
loading elpi/bench/sources/cic/alt_0/kernel_case.mod
loading elpi/bench/sources/cic/alt_0/kernel_inductives.mod
loading elpi/bench/sources/cic/alt_0/kernel_global.mod
loading testttt.mod

Trying to debug but right now it's a guessing game. Thanks in advance.

[gares]

The development of a kernel/refiner for CIC moved to https://github.com/LPCIC/matita
where you can call ./matita/matita/matita -elpi CSC matita/matita/lib/arithmetics/nat.ma
to see it in action. (disclaimer: it is still a moving target, especially the refiner).

This repo is only for the lambda-prolog interpreter itself that is the embedded in matita in the other repo.

We should probably clean up these old tests... so I leave the issue open