Comparator generates different instance names for problem and solution files

[eric-wieser]

With this challenge in challenge.lean:

instance : Inhabited Nat := ⟨37⟩

theorem target : default = 37 := sorry

and this solution.lean

instance : Inhabited Nat := ⟨37⟩

theorem target : default = 37 := rfl

comparator fails with

Exporting #[target, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Challenge
Building Solution
Build completed successfully (3 jobs).
Exporting #[target, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Solution
uncaught exception: Challenge and solution theorem statement do not match: 'target'

presumably because one has type

@default _ instInhabitedNat_challenge = 37

and the other has type

@default _ instInhabitedNat_solution = 37

[hanwenzhu]

This is a Lean problem, not a comparator problem right? Generated instance names can have module name attached

[eric-wieser]

Indeed, but comparator could arrange for the module names to match by renaming or doing a lean build with an explicit module name on the command line.

[hanwenzhu]

I agree something better can be done here because the same Lean script can behave differently depending on the module name. I guess the official answer to this would be to put the instance to a shared Basic.lean and have challenge and solution both import it, or manually write instance instInhabitedNat_challenge : Inhabited Nat := ⟨37⟩ in solution.lean.

[hargoniX]

See comment at #59

[tadamcz]

I agree this is an issue. The workaround described in @hargoniX’s comment (putting the statements in a separate Statement.lean file and importing it into both Challenge and Solution) is a significant imposition. The Comparator user:

• may not control or wish to modify the challenge file
• may be dealing with large numbers of challenge files (e.g. thousands)

Is there something wrong with @eric-wieser's suggestion of passing an identical explicit module name for both Challenge and Solution?

[hargoniX]

Doing so does only fix this one particular instance of the problem and not the general issue that names for auto generated things may differ across challenge and solution files. For example, Lean might generate different matchers, different auxiliary declarations etc. depending on the content.

[eric-wieser]

I think this type of autogenerated declaration is different, because it is not content based. If I pass two files with identical contents to comparator as target and challenge, it will still reject them because of this issue. I don't think that's true of any other failure mode.