Add executor for Lean 4

[int-y1]

Coq can't do I/O. Agda requires a resource-intensive command cabal install Agda. Lean 3 can't generate an executable (but it can compile .lean to .olean for a performance boost). The next best language is Lean 4.

How to test this:

• Install Lean 4 to /opt/lean

  mkdir /opt/lean
  curl --compressed -L "https://github.com/leanprover/lean4/releases/download/v4.0.0-m2/lean-4.0.0-m2-linux.tar.gz" | tar xz -C /opt/lean --strip-components=1
  export PATH="/opt/lean/bin:$PATH"

• Modify .docker.test.py and dmoj/citest.py to just test LEAN4
• 
  (nit: the version is actually 4.0.0-m2)

(Lean 4 has some support for siggrading, so it's possible to host a theorem proving contest)

[dmoj-build]

Can one of the admins verify this patch?

[quantum5]

ok to test

[codecov-commenter]

Codecov Report

Merging #982 (6f274d6) into master (d52800a) will increase coverage by 2.77%.
The diff coverage is 42.10%.

@@            Coverage Diff             @@
##           master     #982      +/-   ##
==========================================
+ Coverage   80.80%   83.58%   +2.77%     
==========================================
  Files         138      139       +1     
  Lines        4695     4714      +19     
==========================================
+ Hits         3794     3940     +146     
+ Misses        901      774     -127     

Impacted Files	Coverage Δ
dmoj/executors/LEAN4.py	35.29% <35.29%> (ø)
dmoj/cptbox/isolate.py	86.77% <100.00%> (+47.28%)	⬆️
dmoj/judge.py	52.83% <0.00%> (+1.25%)	⬆️
dmoj/executors/java_executor.py	85.35% <0.00%> (+2.02%)	⬆️
dmoj/executors/compiled_executor.py	77.71% <0.00%> (+4.00%)	⬆️
dmoj/cptbox/tracer.py	77.33% <0.00%> (+18.34%)	⬆️
dmoj/cptbox/handlers.py	100.00% <0.00%> (+25.00%)	⬆️
dmoj/control.py	100.00% <0.00%> (+64.70%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update d52800a...6f274d6. Read the comment docs.