diff options
Diffstat (limited to 'readme.md')
| -rw-r--r-- | readme.md | 47 |
1 files changed, 41 insertions, 6 deletions
@@ -1,6 +1,6 @@ -# Naproche/ZF +# Felix -Naproche/ZF is an experimental [proof assistant](https://en.wikipedia.org/wiki/Proof_assistant) +Felix is an experimental [proof assistant](https://en.wikipedia.org/wiki/Proof_assistant) based on [set theory](https://en.wikipedia.org/wiki/Set_theory) (and [classical logic](https://en.wikipedia.org/wiki/Classical_logic)). It uses a [controlled language](https://en.wikipedia.org/wiki/Controlled_natural_language) embedded into subset of LaTeX as input format, supporting [literate formalization](https://en.wikipedia.org/wiki/Literate_programming). @@ -78,10 +78,45 @@ their locations as explicit proof gaps and includes them in its authorization summary. Verification always opens a disposable SQLite store. By default Felix uses -the platform's XDG cache directory; `--store PATH` selects an existing parent -directory explicitly, while `--fresh` uses a temporary store that is removed -after the command. `--parseonly` performs source discovery and parsing without -opening a store or invoking Vampire. +the platform's XDG cache directory; `--store PATH` selects an explicit database +file whose parent directory already exists, while `--fresh` uses a temporary +store that is removed after the command. A store is reusable only when its +two-field cache-epoch/theory identity matches this build. An incompatible or +damaged store is never migrated or silently rebuilt: use `--fresh`, select a +new path, or remove the disposable database and verify again. + +The command model has three modes. `--version` prints the version, +`--parseonly` performs authority-free source discovery and parsing without +opening SQLite or invoking Vampire, and ordinary invocation verifies through +the typed checker. Both paths load the packaged final prelude's syntax; Verify +also acquires its sealed semantics. Ordinary modules therefore need no source +import for the prelude dependency. + +Without `--jobs`, verification uses one fewer than the detected logical +processor count, with a minimum of one. A positive `--jobs N` is an exact bound +for live module checkers and one-core Vampire processes. `-t` and `-m` bound +each Vampire request's time and memory. + +Source fixity declarations are line-leading pragmas such as `%! infixl 4`. +User declarations may use literal levels 0 through 7; the two higher internal +levels are reserved. Verification keeps compact proof-independent theorem +authority separate from exact proof/declaration validation. Its authorization +summary lists only direct source axioms and syntactic `Omitted` sites, not +facts that merely inherit their safety. + +`--html DIRECTORY` and `--dump DIRECTORY` observe the same verification. +Dump files are the exact Vampire requests that actually ran and the directory +must be absent or empty. HTML is uncached and is published sequentially in +source order only after complete semantic success; a later output failure +reports the already committed output prefix together with the successful +authorization summary. + +Declarations append atomically and modules expose only sealed syntax and +semantic interfaces. After an ordinary later failure, the successfully checked +declaration prefix remains reusable but the incomplete module has no root. +Compatible stores can reuse rebound parsed artifacts, exact validation, and +complete module roots; source remains authoritative, so an edited proof or +interface is revalidated at the corresponding content boundary. For a list of all options run `stack exec zf -- --help`. |