Lean version support incompatible with LeanDojo tracer #7
Description
Lean version support is limited to < 4.8
However the LeanDojo tracer seems to rely on a more recent lean api
src/lean_dojo/data_extraction/ExtractData.lean
Currently I am trying to use LeanDojo and I have restricted the Lean version to 4.8.0 so that I have the option to use LeanAgent later on
However I'm getting these kinds of errors from the tracer:
ExtractData.lean:341:24: error: invalid field 'get?', the environment does not contain 'Lean.HashMap.get?' env.const2ModIdx has type HashMap Name ModuleIdx ExtractData.lean:341:24: error: invalid field 'get?', the environment does not contain 'Subtype.get?' env.const2ModIdx has type { m // HashMapImp.WellFormed m } ExtractData.lean:342:27: error: invalid field notation, type is not of the form (C ...) where C is a constant modIdx has type ?m.26945 ExtractData.lean:479:41: error: application type mismatch getImports header argument header has type Syntax : Type but is expected to have type TSyntax Lean.Parser.Module.header : Type`
What is the recommended approach to use both of these projects together?