search

isabelle-prover / proving-contest-backends

"proving-contest"-backends for several theorem provers
MIT License
12 stars 5 forks source link

Isabelle judge - qualified constants in the submission lead to timeout #20

Closed maxhaslbeck closed 5 years ago

maxhaslbeck commented 5 years ago

if a submission contains a qualified constant like "Defs.sum" the judge times out.

this is because, "Defs" is renamed to "Defs0", which then is imported by a new theory "Defs" which imports "Defs0" and "OK_Test" and saves the context.

this should be altered, to not renaming the Defs, and calling the "context_saving_theory" "Defs0", then alter the Submission s.t. it imports Defs0 instead of Defs.

maxhaslbeck commented 5 years ago

closed by c72514da3a709268438a1f956d0ff5c62d800be4