Lean backend upgrade

[kappelmann]

What

• More flexible setup mechanism (easy to change Lean version, directory, etc.)
• Better error messaging
• Partial point grading
• Add tests
• Speed up compile process by adding the right flags to the lean compiler
• Full support of the Poller interface (e.g. multiple check entries)

Why

Because the current Lean implementation is lacking all features mentioned in What.

How

• Add variables to setup mechanism
• Use the error messages returned by the lean compiler and add custom ones for axioms
• Invoke the leanchecker for every theorem/lemma found in check.lean.

Testing

• Tests can be executed using tests_run.sh
• I uploaded some submissions (1, 2, 3), and they seem to work.

Notes

• Partial points need to be tested (I was not sure about how to test that)
• By default, Lean is installed to /tmp/lean-grader/<version>. Feel free to change that in variables/lean_version
• Other TODOs: see TODOs in README.md

[maxhaslbeck]

the setup works out of the box, nice. also the deployed judge seems to work fine on the test server. Yet, there are still some problems.

checking submission 82 gives good results but also prints the following errors:

--- Logging error ---
Traceback (most recent call last):
  File "/usr/lib/python3.6/logging/__init__.py", line 995, in emit
    stream.write(msg)
UnicodeEncodeError: 'latin-1' codec can't encode character '\u03a0' in position 47: ordinal not in range(256)
Call stack:
  File "/tmp/lean-grader/3.4.2/grader.py", line 81, in <module>
    logger.info(checker_result.stdout)
Message: 'axiom propext : \u03a0 {a b : Prop}, (a <-> b) -> a = b\ntheorem lemma2 : \u03a0 n : nat, n <= my.sum n\nchecked 523 declarations\n'
Arguments: ()
--- Logging error ---
Traceback (most recent call last):
  File "/usr/lib/python3.6/logging/__init__.py", line 995, in emit
    stream.write(msg)
UnicodeEncodeError: 'latin-1' codec can't encode character '\u03a0' in position 54: ordinal not in range(256)
Call stack:
  File "/tmp/lean-grader/3.4.2/grader.py", line 81, in <module>
    logger.info(checker_result.stdout)
Message: 'axiom i_am_a_cheater : \u03a0 M : nat, Exists (\u03bb N : nat, \u03a0 n : nat, n >= N -> my.sum n >= M)\ntheorem lemma3 : \u03a0 M : nat, Exists (\u03bb N : nat, \u03a0 n : nat, n >= N -> my.sum n >= M)\nchecked 57 declarations\n'
Arguments: ()

do the UnicodeEncodeError s also occur with you? maybe some different python version?

regarding the partial points: http://vmnipkow14.in.tum.de/competitions/submission/82/ your judgement is the following:

{"submission_is_valid": false, 
"messages": [{"where": "submission.lean at line 3, column 0", "what": "WARNING: declaration 'goal1' uses sorry"}, 
   {"where": "check.lean at line 1, column 0", "what": "WARNING: imported file 'submission.lean' uses sorry"},
   {"where": "<unknown> at line 1, column 1", "what": "ERROR: failed to expand macro"}, 
   {"where": "lemma3", "what": "WARNING: Unknown axiom 'i_am_a_cheater' used to prove theorem 'lemma3'."}],
 "checks": [{"name": "lemma1", "result": "error"}, 
   {"name": "lemma2", "result": "ok"}, 
   {"name": "lemma3", "result": "ok_with_axioms"}], "log": ""}

I'm not an Lean expert, but I guess for this submission, the submission should be valid ("submission_is_valid": true) and the result for lemma1 should be "ok_with_axioms", then the frontend would count the submission as "passed" and assign it 1/3 points. it seems that using sorry yields an error in your setup, can you change that?

[kappelmann]

Partial points work now, see http://vmnipkow14.in.tum.de/competitions/submission/82/

[kappelmann]

I do not get the UnicodeEncodeError on my machine. This seems to be a problem with locales. cf

• https://github.com/jupyterhub/jupyterhub/issues/1406
• https://github.com/WordOps/WordOps/issues/11