deducteam / isabelle_dedukti Goto Github PK

Based on my understanding on how this file works, and the files in my Isabelle directory, it seems that Dedukti_Base should be

session Dedukti_Base in "Ex/Base" = Pure +
  sessions
    "Pure-Examples"
  theories
    "Pure-Examples.First_Order_Logic"
    "Pure-Examples.Higher_Order_Logic"

Also, executing
isabelle dedukti_build && isabelle dedukti_import -o export_standard_proofs Dedukti_Base
as proposed by the README no longer complains about not being able to load the theory, but instead that some proof in thm "First_Order_Logic.conjE" is absent.

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

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

After an install with opam, at the make step I have the following problem:

% make && make install
File "commands/dkcheck.ml", line 118, characters 2-7:
Error: Unbound module Cmd
File "commands/dkdep.ml", line 75, characters 2-5:
Error: Unbound module Cmd
File "commands/dkmeta.ml", line 117, characters 2-14:
Error: Unbound module Cmdliner.Cmd
File "commands/dkpretty.ml", line 28, characters 2-5:
Error: Unbound module Cmd
File "commands/dkprune.ml", line 279, characters 2-14:
Error: Unbound module Cmdliner.Cmd
File "commands/dktop.ml", line 15, characters 2-14:
Error: Unbound module Cmdliner.Cmd

I did not find any file with the suffix .Cmd ?

Thanks

Report here but the bug most likely lies in Isabelle proper.

Trying to export up to HOL.Zorn, and got a dependency problem between HOL.Sum_Type and HOL.Product_Type

proof408788 is defined in HOL.Product_Type, used in HOL.Sum_Type but the latter does not reference the former.

ROOT

[...]
session Isabelle_Export in "Ex/Export" = Pure +
  options [export_theory, export_proofs, record_proofs = 2]
  sessions HOL
  theories
    HOL.List

bash

isabelle dedukti_build && isabelle dedukti_import -O "test/main.lp" Isabelle_Export

Appears both on master and on my fork (which supports today's lambdapi)

I'm still quite new and don't know everything about this, so this may be my fault

isabelle dedukti_test fails because $ISABELLE_LAMBDAPI is not set.

Should this variable be set by the user? This is not explained in the README.

In addition, the script lib/Tools/dedukti_test seems to have another problem: because of the use of double quotes, $ISABELLE_LAMBDAPI cannot be set to lambdapi check:

18:55 ~/src/isabelle_dedukti (master) isabelle dedukti_test
Importing theory Pure
Importing theory Tools.Code_Generator
Importing theory HOL.HOL
Importing theory HOL.Ctr_Sugar
Importing theory HOL.Orderings
Importing theory HOL.Groups
Importing theory HOL.Lattices
Importing theory HOL.Set
Importing theory HOL.Fun
Importing theory HOL.Complete_Lattices
Importing theory HOL.Inductive
0:00:46 elapsed time
lambdapi: unknown command `output.lp'.
Usage: lambdapi COMMAND ...
Try `lambdapi --help' for more information.

By using set -x, we get:

19:12 ~/src/isabelle_dedukti (master) lib/Tools/dedukti_test 
+ OUTPUT=output.lp
++ dirname output.lp
+ cd .
++ basename output.lp
+ 'lambdapi check' output.lp
lib/Tools/dedukti_test: ligne 11: lambdapi check : commande introuvable

Finally, a lambdapi.pkg file is missing.

• implicit arguments are printed while they should not
• the option -n make isabelle dedukti_session fail
• fix qualified names so that names from some other session can be found
• use require open for STTfa

Hi Makarius and Michael,
It would make more sense if the repository was owned by Deducteam, rather than by me. I'd like to transfer ownership. Is that OK with both of you?

• Currently, the command isabelle dedukti_generate takes as argument -O main.lp or -O main.dk but no file main.lp or main.dk are generated. This should be replaced by a single option -lp (default being dk output).
• In README.md, references to isabelle dedukti_import should be removed.
• In src/tools.scala, Tools should be removed and Tools2 renamed into Tools.