search

Deducteam / isabelle_dedukti

Isabelle component generating Dedukti proofs
Other
3 stars 4 forks source link

Not all theory files are exported #28

Closed sacerdot closed 1 year ago

sacerdot commented 1 year ago

I have the impression that only the recursive dependencies of Complex_Main can be exported.

Esample of missing theory: HOL/Lattice/Orders.thy

sacerdot commented 1 year ago

Ok, I see. The content of the src/HOL library of Isabelle is not a single session, but multiple ones (see the ROOT file there). The one named HOL is rooted in Complex_Main + Main and thus only their dependencies are exported.

However, one can convert to Dedukti other sessions, even if there are bugs (at least for sessions not in the standard library).

This issue can be closed I think, but bug reports will follow.

fblanqui commented 1 year ago

Hi Claudio. I close this issue. With the merge of #16 it is now possible to export other developments, including those of AFP.