The system
How it fits together
Most components run independently. They use common project records, command handlers and validation formats.
Public programs
Plectis publishes selected programs from a larger private system. The public examples include their input files and can run without access to the private system.
Public repositories and website
The Plectis repository contains the public software. This website explains it through pages generated from the repository records, with links to their sources. The Lean repository contains the mathematics and proof code; Lean's kernel checks the formal proofs. The 21 papers are built in those repositories, and deployment checks that the hosted copies match their source files. If a generated page disagrees with its source, consult that source and report the discrepancy.
Shared records and commands
The following sequence names the records and procedures used to organise a task, execute it and save its results:
The project identifies the working folder. A pattern describes the task, a standard defines its requirements, and a route selects the command. The program performs the work and records events and evidence. An explanation describes the result. The project calls the subsequent incorporation of useful results into maintained records assimilation.