search

Deducteam / Dedukti

Implementation of the λΠ-calculus modulo rewriting
https://deducteam.github.io
Other
200 stars 22 forks source link

dk dep -s fails #321

Open fblanqui opened 8 months ago

fblanqui commented 8 months ago 
16:54 /tmp/export_raw_dk ls
tests_OK_1006.dk               tests_OK_empty.dk
tests_OK_1035.dk               tests_OK_Escaped.dk
tests_OK_225.dk                tests_OK_eta_equality.dk
tests_OK_262_pair_ex_1.dk      tests_OK_for_inductive.dk
tests_OK_292.dk                tests_OK_freevars-constraints.dk
tests_OK_301.dk                tests_OK_identifiers.dk
tests_OK_303.dk                tests_OK_implicitArgs1.dk
tests_OK_330b.dk               tests_OK_implicitArgs2.dk
tests_OK_330.dk                tests_OK_nested_comment_lp.dk
tests_OK_621c.dk               tests_OK_patt.dk
tests_OK_698_abst_impl.dk      tests_OK_private.dk
tests_OK_725.dk                tests_OK_require_symbol.dk
tests_OK_878.dk                tests_OK_symbol.dk
tests_OK_abstractions.dk       tests_OK_sym_decl.dk
tests_OK_append.dk             tests_OK_tail.dk
tests_OK_boolean.dk            tests_OK_type.dk
tests_OK_builtin_succ_zero.dk  tests_OK_varmatch.dk
tests_OK_compute.dk            tests_OK_zero.dk
tests_OK_declared.dk

16:54 /tmp/export_raw_dk dk dep *.dk
tests_OK_identifiers.dko : tests_OK_identifiers.dk 
tests_OK_330.dko : tests_OK_330.dk 
tests_OK_330b.dko : tests_OK_330b.dk 
tests_OK_varmatch.dko : tests_OK_varmatch.dk 
tests_OK_303.dko : tests_OK_303.dk 
tests_OK_freevars-constraints.dko : tests_OK_freevars-constraints.dk 
tests_OK_Escaped.dko : tests_OK_Escaped.dk 
tests_OK_compute.dko : tests_OK_compute.dk 
tests_OK_725.dko : tests_OK_725.dk 
tests_OK_225.dko : tests_OK_225.dk 
tests_OK_eta_equality.dko : tests_OK_eta_equality.dk 
tests_OK_private.dko : tests_OK_private.dk 
tests_OK_262_pair_ex_1.dko : tests_OK_262_pair_ex_1.dk 
tests_OK_1035.dko : tests_OK_1035.dk 
tests_OK_boolean.dko : tests_OK_boolean.dk 
tests_OK_878.dko : tests_OK_878.dk 
tests_OK_621c.dko : tests_OK_621c.dk 
tests_OK_sym_decl.dko : tests_OK_sym_decl.dk 
tests_OK_301.dko : tests_OK_301.dk 
tests_OK_292.dko : tests_OK_292.dk 
tests_OK_builtin_succ_zero.dko : tests_OK_builtin_succ_zero.dk 
tests_OK_zero.dko : tests_OK_zero.dk 
tests_OK_for_inductive.dko : tests_OK_for_inductive.dk 
tests_OK_698_abst_impl.dko : tests_OK_698_abst_impl.dk 
tests_OK_type.dko : tests_OK_type.dk 
tests_OK_require_symbol.dko : tests_OK_require_symbol.dk tests_OK_symbol.dko
tests_OK_patt.dko : tests_OK_patt.dk 
tests_OK_declared.dko : tests_OK_declared.dk 
tests_OK_1006.dko : tests_OK_1006.dk 
tests_OK_implicitArgs2.dko : tests_OK_implicitArgs2.dk 
tests_OK_abstractions.dko : tests_OK_abstractions.dk 
tests_OK_append.dko : tests_OK_append.dk 
tests_OK_tail.dko : tests_OK_tail.dk 
tests_OK_implicitArgs1.dko : tests_OK_implicitArgs1.dk 

16:54 /tmp/export_raw_dk dk dep -s *.dk
dkcheck: internal error, uncaught exception:
         Api.Files.Files_error(_)