Module lean_encoding 

Macros

string_vec 🔒

Helper macro to create Vec from string-like values

Structs

LakeDiagnostic 🔒

A diagnostic reported by lake build, e.g., error: LeanProofs/User/Proof/FooProof.lean:8:2: msg

LeanEncoder

ProofReport 🔒

What lake build reported about the external proof of a single function

Enums

FileKind

LakeSeverity 🔒

LeanFile

Different kinds of Lean files

Functions

check_proofs

Checks the external (lean) proofs of all the def_ids with a single lake build, reporting an error for each proof that fails to check. Returns the results in the same order as def_ids.

constant_deps 🔒

create_file_with_dirs 🔒

Create a file at the given path, creating any missing parent directories.

create_or_truncate_file_with_dirs 🔒

Create or truncate a file at the given path, creating any missing parent directories.

final_project_path 🔒

finalize

find_def 🔒

Returns the 1-based line and column of name in the line that defines it (def <name> ...).

generate_checking_file 🔒

Generates the file that checks that the proof has the type of the VC. The #print axioms is used to reject proofs that (transitively) depend on sorryAx, see ProofReport::status. The file is regenerated even when the VC is cached, so that it is always up to date.

hyperlink_proof

Hyperlinks the proven_externally attribute to the proof’s def in the proof file, so users can easily jump to it. Call this after the Lean files are generated, so that the proof file exists on the first run. The def is found by searching the file, since the user may have edited it; if the file or the def is missing, we link to the first line of the file.

log_proof

We need to record the checking file in Basic.lean (so that it gets checked by lake build), regardless of whether the proof was cached.

namespaced 🔒

parse_lake_output 🔒

Parses the (human readable) output of lake build into a list of diagnostics. Each diagnostic starts with a line <severity>: <file>:<line>:<col>: <message> and extends over subsequent lines until the next diagnostic or a line reporting build progress.

prim_op_lean_name 🔒

project 🔒

project_digest

A digest of the lean sources in the project (skipping build artifacts in .lake) and of the lake configuration. A cached proof is only trusted if this digest is unchanged since the proof was checked, as the proof, or any lemma or dependency it uses, may have been edited in the meantime.

project_path 🔒

proof_name 🔒

proof_statuses 🔒

Determines the status of the external proof of each of the def_ids with a single pass over the diagnostics, dispatching each one to the proof whose checking or proof file it is reported in. Returns the results in the same order as def_ids.

record_proof 🔒

rename_dir_contents 🔒

Renames all files and directories from ‘src’ to ‘dst’

run_lake_build 🔒

Runs a single lake build on the checking files of all the def_ids

sort_name_fragment 🔒

vc_name 🔒