-
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathREPORT.a2ml
More file actions
57 lines (57 loc) · 8.05 KB
/
Copy pathREPORT.a2ml
File metadata and controls
57 lines (57 loc) · 8.05 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
;; SPDX-License-Identifier: MPL-2.0
;; Auto-generated by scripts/canonical-proof-suite-runner.sh
;; This is the latest run output. Per-entry detail lives in
;; proofs/canonical-proof-suite/<id>.sidecar.a2ml.
(canonical-proof-suite-report
(metadata
(project "007")
(suite-spec-version "1.0")
(run-utc "2026-04-27T18:34:38Z")
(host "fedora")
(manifest "audits/canonical-proof-suite/MANIFEST.a2ml"))
(summary
(total 35)
(passing 35)
(regressed 0)
(failing 0)
(in-progress 0)
(stub 0)
(not-started 0)
(prover-missing 0))
(entries
(entry (id "M1") (status "passing") (elapsed-ms 8482) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/M1InfinitudeOfPrimes.idr") (semantic-check "verified"))
(entry (id "M2") (status "passing") (elapsed-ms 6143) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M2_lagrange.v") (semantic-check "verified"))
(entry (id "M3") (status "passing") (elapsed-ms 2148) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M3_ivt.v") (semantic-check "verified"))
(entry (id "M4") (status "passing") (elapsed-ms 2877) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M4_compactness_unit_interval.v") (semantic-check "verified"))
(entry (id "M5") (status "passing") (elapsed-ms 1190) (prover "agda") (kernel-version "Agda version 2.8.0") (proof-file "proofs/canonical-proof-suite/M5-yoneda.agda") (semantic-check "verified"))
(entry (id "S1") (status "passing") (elapsed-ms 385) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S1_noether_energy.v") (semantic-check "verified"))
(entry (id "S2") (status "passing") (elapsed-ms 414) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S2_gauss_law.v") (semantic-check "verified"))
(entry (id "S3") (status "passing") (elapsed-ms 1637) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S3_h_theorem_binary.v") (semantic-check "verified"))
(entry (id "S4") (status "passing") (elapsed-ms 1286) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S4_heisenberg_discrete.v") (semantic-check "verified"))
(entry (id "S5") (status "passing") (elapsed-ms 1272) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S5_shannon_source_coding.v") (semantic-check "verified"))
(entry (id "E1") (status "passing") (elapsed-ms 3863) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E1_lyapunov_ndim.v") (semantic-check "verified"))
(entry (id "E2") (status "passing") (elapsed-ms 3465) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr") (semantic-check "verified"))
(entry (id "E3") (status "passing") (elapsed-ms 180) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E3_cantilever_deflection.v") (semantic-check "verified"))
(entry (id "E4") (status "passing") (elapsed-ms 3528) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr") (semantic-check "verified"))
(entry (id "E5") (status "passing") (elapsed-ms 170) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E5_auth_key_binding.v") (semantic-check "verified"))
(entry (id "M6") (status "passing") (elapsed-ms 172) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M6_deduction_theorem.v") (semantic-check "verified"))
(entry (id "S6") (status "passing") (elapsed-ms 230) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S6_mass_action.v") (semantic-check "verified"))
(entry (id "E6") (status "passing") (elapsed-ms 253) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E6_cstr_mass_balance.v") (semantic-check "verified"))
(entry (id "M7") (status "passing") (elapsed-ms 212) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M7_linearity_of_expectation.v") (semantic-check "verified"))
(entry (id "M8") (status "passing") (elapsed-ms 698) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M8_rank_nullity.v") (semantic-check "verified"))
(entry (id "M9") (status "passing") (elapsed-ms 425) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M9_unique_factorization.v") (semantic-check "verified"))
(entry (id "M10") (status "passing") (elapsed-ms 187) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M10_knot_composition_monoid.v") (semantic-check "verified"))
(entry (id "M11") (status "passing") (elapsed-ms 691) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M11_pigeonhole.v") (semantic-check "verified"))
(entry (id "E7") (status "passing") (elapsed-ms 145) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E7_carnot_efficiency.v") (semantic-check "verified"))
(entry (id "S7") (status "passing") (elapsed-ms 179) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S7_lorentz_velocity_addition.v") (semantic-check "verified"))
(entry (id "E8") (status "passing") (elapsed-ms 171) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E8_nyquist_shannon.v") (semantic-check "verified"))
(entry (id "M12") (status "passing") (elapsed-ms 205) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M12_dominated_convergence.v") (semantic-check "verified"))
(entry (id "S8") (status "passing") (elapsed-ms 171) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S8_hardy_weinberg.v") (semantic-check "verified"))
(entry (id "E9") (status "passing") (elapsed-ms 194) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E9_newton_convergence.v") (semantic-check "verified"))
(entry (id "M13") (status "passing") (elapsed-ms 209) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M13_hahn_banach.v") (semantic-check "verified"))
(entry (id "M14") (status "passing") (elapsed-ms 174) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M14_max_flow_min_cut.v") (semantic-check "verified"))
(entry (id "S9") (status "passing") (elapsed-ms 171) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S9_chandrasekhar.v") (semantic-check "verified"))
(entry (id "S10") (status "passing") (elapsed-ms 172) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S10_r_naught_threshold.v") (semantic-check "verified"))
(entry (id "E10") (status "passing") (elapsed-ms 144) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E10_bathtub_reliability.v") (semantic-check "verified"))
(entry (id "E11") (status "passing") (elapsed-ms 165) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
))