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 22 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.

Standalone by default

Most components do not call each other. They use the common records and procedures described above. Where components are connected, their pages name the connection.

Local and self-contained

Running a component writes into a .microcosm/ folder beside your project. It doesn't change your source files and doesn't make external calls. The saved records include links to the inputs and checks behind each result.