search

isabelle-prover / proving-contest-backends

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

upgrade to lean-community (3.16.2) #32

Closed kappelmann closed 4 years ago

kappelmann commented 4 years ago

What

  1. Upgrade lean to use the community supported lean version (3.16.2 in this commit).
  2. Update the download URL for mathlib
  3. Make tests more resilent and update them as the french quoting bug got (kind of) solved.
  4. Update README with a gotcha note
  5. Add testcases for computable and noncomputable definitions.

Why

Because things move fast and break even faster.

How

  1. Update download URLs
  2. Make lean version a commit revision number
  3. For checking whether the user gives a computable definition, it suffices to assign the user-defined function to a definition in the check file.
maxhaslbeck commented 4 years ago

Thanks, works out of the box.

But we still have a problem regarding different versions of Lean. That's maybe not a problem of this PR but you could make life easier with a bit of work.

In the frontend we have the language "LEA" registered, and at the moment it stands for "Lean 3.4.2". So if users submit solutions for it, it should be graded with that version. also if you look at the tasks from last year, it should be possible to regrade them successfully. On the other hand, we would like to state the "AllTime" problems and also the new problems for upcoming contests in the "Lean 3.16.2" language, and judge it appropriately.

For different Isabelle versions, we introduced different languages "ISA", "I19", "I20", and run separate judge instances for them. We could do the same for Lean, I introduced "LEA" and "L16" meaning "Lean3.4.2" and "Lean3.16.2" respectively. That way, we can update the "AllTime" problems by providing additional Task_Resources (i.e. defs, template, check, public_check theories) for "L16", then the users can decide which version of the ITP they use.

As a quick fix, on the backend side, we than could run several instances of the Lean prover (one for "LEA", one for "L16" . problem is, that this string is hard coded. Could you also pull that out into a file in the Lean/variables folder? That's only a quick fix, it would be better if a judge can poll tasks from different provers, but that would require a change in the restapi, and we will take care of that in the next iteration.

In general it would be nice to redesign the system with not only different provers but also different versions in mind. That was a mistake when designing the original system.