rzk
An experimental proof assistant for synthetic ∞-categories
https://github.com/rzk-lang/rzk#readme
Version on this page: | 0.7.3 |
LTS Haskell 22.43: | 0.7.5 |
Stackage Nightly 2024-11-30: | 0.7.5 |
Latest on Hackage: | 0.7.5 |
rzk-0.7.3@sha256:1b8f630cfb820d647f0144dc71d79e5dcf7f60cf745f4d959915056f3ffeb81c,5101
Module documentation for 0.7.3
- Free
- Language
- Rzk
- Rzk.Format
- Rzk.Main
- Rzk.Project
- Rzk.TypeCheck
rzk
An experimental proof assistant for synthetic ∞-categories.
See README at https://github.com/rzk-lang/rzk#readme.
Changes
Changelog for rzk
All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog, and this project adheres to the Haskell Package Versioning Policy.
v0.7.3 — 2023-12-16
Fixes:
- Fix overlapping edits in the formatter, hopefully making it idempotent (see #160);
- Fix formatter crashing the language server (see #161);
- Avoid unnecessary typechecking when semantics of a file has not changed (see #159);
- Stop typechecking after the first parse error (avoid invalid cache) (see
68ab0b4
);
Other:
- Add unit tests for the formatter (see #157);
v0.7.2 — 2023-12-12
Fixes:
- Fixes for
rzk format
: - Throw an error when
rzk.yaml
’sinclude
is empty (see #154);
Changes to the Rzk website:
- Support multiple languages in the documentation (see #150);
- English is the default;
- Russian documentation is partially translated and is available at http://rzk-lang.github.io/rzk/ru/;
- Add a blog (see #153 and
e438820
);- The blog is not versioned and is always available at https://rzk-lang.github.io/rzk/en/blog/;
- Add a new Other proof assistants for HoTT page (also in Russian);
- Add a new Introduction to Dependent Types page (also in Russian)
- Add (default) social cards
- Integrate ToC on the left
- Use Inria Sans for English, PT Sans for Russian
v0.7.1 — 2023-12-08
- Fix default build to include Rzk Language Server (
rzk lsp
) (see9b78a15
); - Apply formatting to
recId.rzk.md
example (see4032724
);
v0.7.0 — 2023-12-08
Major changes:
- Add an experimental
rzk format
command (by Abdelrahman Abounegm, with feedback by Fredrik Bakke (see sHoTT#142) and Nikolai Kudasov):- Automatically format files, partially automating the Code Style of the sHoTT project
- Notable features:
- Adds a space after the opening parenthesis to help with the code tree structure
- Puts the definition conclusion (type, starting with
:
) and construction (body, starting with:=
) on new lines - Adds a space after the
\
of a lambda term and around binary operators (like,
) - Moves binary operators to the beginning of the next line if they appear at the end of the previous one.
- Replaces common ASCII sequences with their Unicode equivalent
- A CLI subcommand (
rzk format
) with--check
and--write
options
- Known limitations
- The 80 character line limit is currently not enforced due to the difficulty of determining where to add line breaks (for reference, check out this post by a Dart
fmt
engineer) - Fixing indentation is not yet implemented due to the need for more semantics than the lexer provides to determine indentation level.
- There may be rare edge cases in which applying the formatter twice could result in additional edits that were not detected the first time.
- The 80 character line limit is currently not enforced due to the difficulty of determining where to add line breaks (for reference, check out this post by a Dart
Minor changes:
v0.6.7 — 2023-10-07
- Fix build on some systems (fix
BNFC:bnfc
executable dependency, see #125) - Improve Rzk Playground (see #124 by @deemp):
- Add
snippet_url
parameter - Migrated from NextJS to Vite
- Use
setText
onparams
attribute
- Add
- Slightly improve documentation:
v0.6.6 — 2023-10-02
- Fix builds on Windows (and macOS) (see #121)
v0.6.5 — 2023-10-01
This version contains mostly intrastructure improvements:
- Typecheck using
rzk.yaml
if it exists (see #119) - Update Rzk Playground and Nix Flake (see #84)
- Rzk Playground now uses CodeMirror 6 and NextJS
miso
dependency is dropped- GHCJS 9.6 is now used
- Support
snippet={code}
orcode={code}
param (see #118)- Support for
snippet_url={URL}
is temporarily dropped
- Support for
- Update to GHC 9.6, latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see #116)
- Add logging for Rzk Language Server (see #114)
Fixes:
- Fix error messages in Rzk Playground (see #115)
v0.6.4 — 2023-09-27
This version improves the stucture of the project, in particular w.r.t dependencies:
- Add custom snapshot and explicit lower bounds (see #108)
v0.6.3 — 2023-09-27
This version contains a fix for the command line interface of rzk
:
-
Fix command line
rzk typecheck
(see #106)- Previous version ignored failures in the command line (the bug was introced when allowing better autocompletion in LSP).
v0.6.2 — 2023-09-26
This version contains some improvements in efficiency and also to the language server:
- Improve efficiency of the tope solver, applying LEM for directed interval only as a fallback option (see #102)
- Support autocompleting definitions from previous modules (see #102)
- Well-typed definitions from the same module also work if the module is only partially well-typed!
- Improve information order in the error messages given in LSP diagnostics (see #104)
v0.6.1 — 2023-09-24
This version contains a minor fix:
- Catch exceptions in the parser, fixing LSP for files where layout resolver fails (see #99).
v0.6.0 — 2023-09-23
This version introduces a proper LSP server with basic support for incremental typechecking and some minor improvements:
- LSP server with incremental typechecking (see #95);
- Improve error messages for unclosed
#section
and extra#end
(see #91).
v0.5.7 — 2023-09-21
This version contains two fixes (see #88) for issues discovered in rzk-lang/sHoTT#30:
- We now only generate well-typed LEM instances in the tope solver, speeding up significantly.
- We fix $\eta$-rule for product cubes, to not get stopped by reflexive equality topes like $\langle \langle \pi_1 (t_{12}), \pi_2 (t_{12}) \rangle, t_3 \rangle \equiv \langle t_{12}, t_3 \rangle$.
v0.5.6 — 2023-09-19
This version fixes the behaviour of glob (see 77b7cc0
).
v0.5.5 — 2023-09-19
This version contains Unicode and tope logic-related fixes:
- Fix (add missing checks) for subshapes (see #85);
- Allow to handle wildcards in
rzk
itself (see #83); - Fix Unicode on machines with non-standard locales (see #82);
- Specify
happy
andalex
as build tools to fix cabal build from Hackage (see #80). - Add configuration for MkDocs plugin for Rzk (see #79).
v0.5.4 — 2023-08-19
This version contains minor improvements:
- Improve typechecking by trying an easier unification strategy first (see #76);
- Update GitHub Action for Nix (see #74).
v0.5.3 — 2023-07-12
This version contains a few minor improvements:
- Allow patterns in dependent function types (see #67);
- Hint about possible shape coercions (see #67);
- Enable doctests (see #68);
- Improve documentation (add recommended installation instructions via VS Code)
- Migrate from
fizruk
torzk-lang
organisation on GitHub (seeee0d063
); - Speed up GHCJS build with Nix (see #66);
v0.5.2 — 2023-07-05
This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit:
- Support some Unicode syntax (see #61);
- Support curly braces syntax for code blocks (see #64);
- Update documentation a bit (see 07b520a6 and 7cc7f383);
- Factor out Pygments highlighting to https://github.com/rzk-lang/pygments-rzk;
- Use new cache action for Nix (see #60).
v0.5.1 — 2023-06-29
This version fixes Unit
type and makes some changes to documentation:
- Fix computation for
Unit
(see 2f7d6295); - Update documentation (see ea2d176b);
- Use mike to deploy versioned docs (see 99cf721a);
- Replace MkDocs hook with the published plugin (see #58);
- Switch to Material theme for MkDocs (see #57);
- Fix links to
*.rzk.md
inmkdocs.yml
(see 8ba1c55b);
v0.5 — 2023-06-20
This version contains the following changes:
Unit
type (withunit
value) (see ede02611 and bf9d6cd9;- Add basic tokenizer support via
rzk tokenize
(see #53); - Add location information for shadowing warnings and duplicate definition errors (see bf9d6cd9).
v0.4.1 — 2023-06-16
This is version contains minor changes, primarily in tools around rzk:
- Add
rzk version
command (see f1709dc7); - Add action to release binaries (see 9286afae);
- Automate SVG rendering in MkDocs (see #49);
- Read
stdin
when no filepaths are given (see 936c15a3); - Add Pygments highlighting (see 01c2a017, cbd656cc, 5220ddf9, 142ec003, 5c7425f2);
- Update HighlightJS config for rzk v0.4.0 (see 171ee63f);
v0.4.0 — 2023-05-18
This version introduces sections and variables. The feature is similar to Variable
command in Coq. An important difference, however, is that rzk
does not allow definitions to use variables implicitly and adds uses (...)
annotations to ensure such dependencies are not accidental.
- Variables and sections (Coq-style) (see #38);
Minor improvements:
- Add flake, set up nix and cabal builds, cache nix store on CI (see #39);
- Apply stylish-haskell (see 7d42ef62);
v0.3.0 — 2023-04-28
This version introduces an experimental feature for generating visualisations for simplicial terms in SVG.
To enable rendering, enable option "render" = "svg"
(to disable, "render" = "none"
):
#set-option "render" = "svg" -- enable rendering in SVG
Minor changes:
- Exit with non-zero code upon a type error (see b135c4fb)
- Fix external links and some typos in the documentation
Fixes:
- Fixed an issue with tope solver when context was empty (see 6196af9e);
- Fixed #33 (missing coherence check for restricted types).
v0.2.0 - 2023-04-20
This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0.
Language
Syntax is almost entirely backwards compatible with version 0.1.0. Typechecking has been fixed and improved.
Breaking Changes
The only known breaking changes are:
- Terms like
second x y
which previous have been parsed assecond (x y)
now are properly parsed as(second x) y
. - It is now necessary to have at least a minimal indentation in the definition of a term after a newline.
- Unicode syntax is temporarily disabled, except for dependent sums and arrows in function types.
- The restriction syntax
[ ... ]
now has a slightly different precedence, so some parentheses are required, e.g. in(A -> B) [ phi |-> f]
or(f t = g t) [ phi |-> f]
. - Duplicate top-level definitions are no longer allowed.
Deprecated Syntax
The angle brackets for extension types are supported, but deprecated,
as they are completely unnecessary now: <{t : I | psi t} -> A t [ phi t |-> a t ]>
can now be written as {t : I | psi t} -> A t [ phi t |-> a t]
or even (t : psi) -> A t [ phi t |-> a t ]
.
Syntax Relaxation
Otherwise, syntax is now made more flexible:
-
Function parameters can be unnamed:
A -> B
is the same as(_ : A) -> B
. -
Angle brackets are now optional:
{t : I | psi t} -> A t [ phi t |-> a t ]
-
Nullary extension types are possible:
A t [ phi t |-> a t ]
-
Lambda abstractions can introduce multiple arguments:
#def hom : (A : U) -> A -> A -> U := \A x y -> (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]
-
Parameters can be introduced simultaneously for the type and body. Moreover, multiple parameters can be introduced with the same type:
#def hom (A : U) (x y : A) : U := (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]
-
Restrictions can now support multiple subshapes, effectively internalising
recOR
:#def hom (A : U) (x y : A) : U := (t : Δ¹) -> A [ t === 0_2 |-> x, t === 1_2 |-> y ]
-
There are now 3 syntactic versions of
refl
with different amount of explicit annotations:refl
,refl_{x}
andrefl_{x : A}
-
There are now 2 syntactic versions of identity types (
=
):x = y
andx =_{A} y
. -
recOR
now supports alternative syntax with an arbitrary number of subshapes:recOR( tope1 |-> term1, tope2 |-> term2, ..., topeN |-> termN )
-
Now it is possible to have type ascriptions:
t as T
. This can help with ensuring types of subexpressions in parts of formalisations, or to upcast types. -
New (better) commands are now supported:
-
#define <name> (<param>)* : <type> := <term>
— same as#def
, but with full spelling of the word -
#postulate <name> (<param>)* : <type>
— postulate an axiom -
#check <term> : <type>
— typecheck an expression against a given type -
#compute-whnf <term>
— compute (WHNF) of a term -
#compute-nf <term>
— compute normal form of a term -
#compute <term>
— alias for#compute-whnf
-
#set-option <option> = <value>
— set a (typechecker) option:#set-option "verbosity" = "silent"
— no log printing#set-option "verbosity" = "normal"
— log typechecking progress#set-option "verbosity" = "debug"
— log every intermediate action (may be useful to debug when some definition does not typecheck)
-
#unset-option <option>
— revert option’s value to its default
-
Simple Shape Coercions
In some places, shapes (cube indexed tope families) can be used directly:
-
In function parameters:
(Λ -> A) -> (Δ² -> A)
is the same as({(t, s) : 2 * 2 | Λ (t, s)} -> A) -> ({(t, s) : 2 * 2 | Δ²} -> A)
-
In parameter types of lambda abstractions:
\((t, s) : Δ²) -> ...
is the same as\{(t, s) : 2 * 2 | Δ² (t, s)} -> ...
Better Type Inference
-
It is now not required to annotate point variables with tope restrictions, the typechecker is finally smart enough to figure them out from the context.
-
It is now possible to simply write
refl
in most situations. -
It is now possible to omit the index type in an identity type:
x = y
Better output and error message
The output and error messages have been slightly improved, but not in a major way.
Internal representation
A new internal representation (a version of second-order abstract syntax) allows to stop worrying about name captures in substitutions, so the implementation is much more trustworthy. The new representation will also allow to bring in higher-order unification in the future, for better type inference, matching, etc.
New representation also allowed annotating each (sub)term with its type to avoid recomputations and some other minor speedups. There are still some performance issues, which need to be debugged, but overall it is much faster than version 0.1.0 already.