I have a couple of Lean projects where the sorries live across multiple files, but comparator today only takes one challenge and solution file.
One example that works well enough today, but is a tad bit clunky, is to import them all into a single file, similar to a module export file.
-- challenge.lean
import Challenge.FileA
import Challenge.FileB
-- config.json
{
"challenge_module": "Challenge",
"solution_module": "Solution",
"theorem_names": ["comm", "assoc"],
"permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
"enable_nanoda": false
}
Alternatively, lean4export supports multiple outputs, so comparator could directly allow specifying multiple challenges and solutions:
-- config.json
{
"challenge_modules": ["ChallengeA", "ChallengeB"],
"solution_modules": ["SolutionA", "SolutionB"],
"theorem_names": ["comm", "assoc"],
"permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
"enable_nanoda": false
}
Or do it as a dictionary pair, if one is worried about making sure the challenge and solution line up.
I have a vibed up draft here for that - master...rusch95:comparator:multi-module-checks - for checking that it's a straightforward enough change, though I think there's a couple of edge cases to do it safely.
Thoughts?
I have a couple of Lean projects where the sorries live across multiple files, but comparator today only takes one challenge and solution file.
One example that works well enough today, but is a tad bit clunky, is to import them all into a single file, similar to a module export file.
Alternatively, lean4export supports multiple outputs, so comparator could directly allow specifying multiple challenges and solutions:
Or do it as a dictionary pair, if one is worried about making sure the challenge and solution line up.
I have a vibed up draft here for that - master...rusch95:comparator:multi-module-checks - for checking that it's a straightforward enough change, though I think there's a couple of edge cases to do it safely.
Thoughts?