# Felix

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


## Example

```latex
\begin{theorem}[Cantor]\label{cantor}
    There exists no surjection from $A$ to $\pow{A}$.
\end{theorem}
\begin{proof}
    Suppose not.
    Consider a surjection $f$ from $A$ to $\pow{A}$.
    Let $B = \{a \in A \mid a\notin f(a)\}$.
    Then $B\in\pow{A}$.
    Take an element $a'$ of $A$ such that $f(a') = B$ by \cref{surj}.
    Now $a' \in B$ iff $a' \notin f(a') = B$.
    Contradiction.
\end{proof}
```


## Development

### Prerequisites

We rely on [Vampire](https://vprover.github.io/) to discharge proof tasks.

You may also need to install `zlib` on certain operating systems.
For example, on Ubuntu you can install the development version of
`zlib` by running `sudo apt install zlib1g-dev`.

#### Obtaining Vampire

Felix and the included library are tested with Vampire at
[commit 367732686](https://github.com/vprover/vampire/commit/3677326861181f990ce3ef461e90471ba9749225).
Its version output describes it as a “Release build”; that is the build mode,
not the tagged Git release.

Build that commit by following the instructions in Vampire’s `README.md` and make sure that the resulting binary is available as `vampire` on your `$PATH` (running `vampire --version` should identify the tested revision).
If you have multiple versions of Vampire installed, you can export the `$NAPROCHE_ZF_VAMPIRE` environment variable to choose a specific version,
e.g. by adding
```
export NAPROCHE_ZF_VAMPIRE="/absolute/path/to/vampire"
```
to your shell configuration.

### Building

This project uses [Stack](http://haskellstack.org/) to manage Haskell libraries and GHC.
You can install Stack and other Haskell tooling using [GHCup](https://www.haskell.org/ghcup/). Follow the GHCup install instructions and then use `ghcup tui` to install Stack.
Stack should install the correct GHC version when you first try to build the software. You can also use GHCup to install the Haskell Language Server, which enables IDE features in some text editors. For VS Code you also need to install the [Haskell extension](https://marketplace.visualstudio.com/items?itemName=haskell.haskell).

You can build the project using `stack build` in the root directory of this project.

Supported platforms are Linux x86-64 and macOS AArch64/x86-64.
Support for Windows is currently untested, but using [WSL2](https://learn.microsoft.com/en-us/windows/wsl/) may work.


### Checking individual files

After running `stack build` you can run the program with `stack exec zf -- <FILENAME>` in the root directory of this project.
The double hyphens `--` separate the arguments of `stack`
from the arguments of the proof checker. Here's an example invocation:

```
stack exec zf -- library/set.tex --log
```

Successful commands exit with status 0. A rejected verification exits with
status 1, while a prover or protocol failure exits with status 2. Diagnostics
are written to stderr. A successful run with `Omitted` proof steps reports
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 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 approximately one third of the detected
logical processor count: `max 1 ((detected + 1) div 3)`. A positive `--jobs N`
is an exact bound for live module checkers and Vampire invocations. Each
invocation runs a two-worker CASC portfolio. `-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`.


### Checking the entire standard library

Run `make lib` to check the file `library/everything.tex`.


### Compiling the PDF of the standard library

```
cd latex && xelatex stdlib.tex
```

### Setting up other formalization environments

When looking for imported files, the following list of base directories is considered (in descending priority):

- the current working directory `.`
- the directory `./library`, which you can override with the environment variable `NAPROCHE_LIB`
- the directory `./debug`


### Running the tests

There are a few [golden tests](https://hackage.haskell.org/package/tasty-golden-2.3.4/docs/Test-Tasty-Golden.html)
that compare the output of the program to previously accepted output.
Run the non-accepting test suite with

```
make test
```

It fails if the output differs from the existing golden files. After reviewing
an intentional output change, explicitly update the golden files with

```
make golden
```


### Building Haskell documentation

Running `stack haddock` will build the project together with its documentation,
placing the rendered HTML files into `haddocks/`.


### Profiling

The following makes sure that stack uses a dedicated directory
to cache the profiled version of all dependencies. Otherwise
switching between profiled and unprofiled builds will cause
lots of recompilation.

```
stack --work-dir .stack-work-profile --profile build
```

Basic time profiling:

```
stack --work-dir .stack-work-profile exec --profile zf -- library/ordinal.tex +RTS -p
```

If you have [ghc-prof-flamegraph](https://hackage.haskell.org/package/ghc-prof-flamegraph) installed
(e.g. after running `cabal install ghc-prof-flamegraph`), you can generate an interactive `zf.prof.svg` from the `.prof` file
by running the following:

```
ghc-prof-flamegraph zf.prof
```


### Debugging

Logical rejections and indeterminate prover results include the failed TPTP task; protocol and process failures include protocol or process diagnostics.
Use `--dump` to write the exact requests sent to Vampire. A failed run retains
only the requests that were executed before the failure. The destination must
be absent or empty; Felix owns the complete directory for that run. `make dump`
creates and prints a fresh temporary destination unless `DUMP_DIR` is supplied.

```sh
dump_dir=$(mktemp -d "${TMPDIR:-/tmp}/felix-dump.XXXXXX")
printf 'Writing dump to %s\n' "$dump_dir"
stack exec zf -- file-that-fails.tex --dump "$dump_dir"
```

You can then run Vampire manually on one of those files.

```sh
vampire --input_syntax tptp --mode casc "$dump_dir/1.p"
```