search

LPCIC / elpi

Embeddable Lambda Prolog Interpreter
GNU Lesser General Public License v2.1
285 stars 36 forks source link

Changes since December #8

Open krpcannon opened 7 years ago

krpcannon commented 7 years ago

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 commented 7 years ago

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