1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
# Naproche/ZF
Naproche/ZF 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 automated theorem provers like
[Vampire](https://vprover.github.io/)
and
[E](https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html)
to discharge proof tasks.
#### Obtaining Vampire
The default prover is Vampire and the included library is written against a specific release of Vampire.
Currently the library uses [Vampire 4.7](https://github.com/vprover/vampire/releases/tag/v4.7).
<!--You can find Linux binaries and source releases [on GitHub](https://github.com/vprover/vampire/releases).-->
On non-Linux platforms you may need to install Vampire by compiling from source.
Download the source code release and follow the instructions in Vampire’s `README.md` and make sure that the resulting binary is available as `vampire` on your `$PATH`.
If you have multiple versions of Vampire installed, you can export the `$NAPROCHE_VAMPIRE` environment variable to choose a specific version,
e.g. by adding
```
export NAPROCHE_VAMPIRE="/absolute/path/to/vampire_4.7"
```
to your shell configuration.
#### Obtaining E
You can usually install a reasonably up-to-date version of E via your system’s package manager
(e.g. via `apt-get install eprover` on Ubuntu and `brew install eprover` on macOS).
Alternatively, you can build E [from source](https://github.com/eprover/eprover).
By default whichever `eprover` is on your `$PATH` will be used,
but you can override the default executable using the `NAPROCHE_EPROVER` environment variable.
### 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 --uncached
```
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 in the command line
- the user library directory, set with the environment variable `NAPROCHE_LIB`, defaulting to `~/formalizations`
- the source code library directory, set with the environment variable `NAPROCHE_SCR_LIB`, defaulting to `~/code/zf/library`
- the source code examples directory, set with the environment variable `NAPROCHE_SCR_EXAMPLES`, defaulting to `~/code/zf/examples`
### 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.
You can run the tests with `stack test`, which will fail if the output differs from the existing golden files.
Run
```
make test
```
or, equivalently
```
stack test --test-arguments "--accept"
```
to update the golden files.
### 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 --uncached +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
If verification fails, then the failed TPTP encoded task is dumped to stderr.
You can redirect that output to a file to experiment with it.
```
stack exec zf -- file-that-fails.tex 2> debug/fail.p
```
You can then run provers manually on that file.
```
eprover --auto --soft-cpu-limit=10 --memory-limit=5000 --silent --proof-object debug/fail.p
vampire --mode casc debug/fail.p
```
You can also dump all prover task by passing, e.g. `--dump ./dump` (the `.gitignore` is set up to ignore files in this specific directory).
|
