Okay this adds a very basic version (it isn't tested yet. to run it you need to remove the sys.exit line)
The idea is the following:
1) run lean check.lean -E check.out --only-export=main_theorem to compile the proof object output from the check.lean file. check.lean contains a main_theorem which checks if the correct theorem was provided
2) run leanchecker check.out main_theorem -- this checks the proof objects and outputs all used axioms
I guess 1) should just produce the file, and no output on stdout at all. 2) might produce three of the following theorems propext, classical.choice and quot.sound.
1) needs to run in a VM, or container or similar. There is no way in Lean to avoid calling meta-functions. The problem is that they have full access to the file system, they can shut down the prover and output arbitrary data. I think leanchecker shouldn't be a problem at all.
Okay this adds a very basic version (it isn't tested yet. to run it you need to remove the
sys.exitline)The idea is the following:
1) run
lean check.lean -E check.out --only-export=main_theoremto compile the proof object output from thecheck.leanfile.check.leancontains amain_theoremwhich checks if the correct theorem was provided2) run
leanchecker check.out main_theorem-- this checks the proof objects and outputs all used axiomsI guess 1) should just produce the file, and no output on stdout at all. 2) might produce three of the following theorems
propext,classical.choiceandquot.sound.1) needs to run in a VM, or container or similar. There is no way in Lean to avoid calling meta-functions. The problem is that they have full access to the file system, they can shut down the prover and output arbitrary data. I think
leancheckershouldn't be a problem at all.