feat: JSON verification reports#50
Conversation
| let reports ← (theoremNames.map (·, "theorem") ++ definitionNames.map (·, "definition")).mapM fun (n, k) => do | ||
| let (t, d) := if k == "theorem" then (#[n], definitionNames) else (#[], #[n]) | ||
| let (cat, msg) := match Comparator.compareAt challenge solution t d (← primitiveTargets) with | ||
| | .error e => (some "comparison", some e) | ||
| | .ok () => match Comparator.checkAxioms solution t d legalAxioms with | ||
| | .error e => (some "axioms", some e) | ||
| | .ok () => (none, none) | ||
| return targetReport n k cat msg | ||
|
|
||
| let mut result := { reports } | ||
| writeReport result | ||
|
|
||
| let fails := reports.filter (·.failureCategory.isSome) | ||
| if !fails.isEmpty then | ||
| let msg := fails.foldl (init := "Some targets failed:\n") fun acc o => | ||
| acc ++ s!"- {o.target}: {o.failureMessage.get!}\n" | ||
| throw <| .userError msg | ||
|
|
||
| let mut errs := #[] | ||
| if ← getNanodaEnabled then | ||
| runNanoda solutionExport | ||
| runKernel solution | ||
| try runNanoda solutionExport |
There was a problem hiding this comment.
This file looks in general a little oddly formatted, could you try sticking more to a standard code style from either core or Mathlib?
| let unpermittedAxioms := transitiveAxioms.filter (!legalAxioms.contains ·) | ||
| { target := n, targetKind := k, failureCategory := cat, failureMessage := msg, unpermittedAxioms, transitiveAxioms : TargetReport } | ||
|
|
||
| let reports ← (theoremNames.map (·, "theorem") ++ definitionNames.map (·, "definition")).mapM fun (n, k) => do |
There was a problem hiding this comment.
This loop has the same performance issue as checking each constant in the kernel individually. Suppose theoremNames is large and contains a lot of transitive dependencies (a lot of which are most likely going to be shared if they are coming from the same area of mathematics). Running the comparison functions on each of them is going to re-check the entire dependency closure O(|theoremNames|) times instead of just once. This is not going to be a noticeable performance diff for challenges with a small amount of theorems but if a user is interested in massively batching comparison this will slow the checking time down massively.
augustepoiroux
force-pushed
the
upstream/json-verification-report
branch
from
74b0a8b to
7dc4553
Compare
2 participants
Implement optional verification output in JSON format.
Key Changes
JSON Fields Summary
unpermittedAxioms: Transitive axioms used by the target that are not legal.transitiveAxioms: List of all transitive axioms used by the target.