rzk-0.9.1: rzk.cabal
cabal-version: 2.0
-- This file has been generated from package.yaml by hpack version 0.39.1.
--
-- see: https://github.com/sol/hpack
name: rzk
version: 0.9.1
synopsis: An experimental proof assistant for synthetic ∞-categories
description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
category: Dependent Types
homepage: https://github.com/rzk-lang/rzk#readme
bug-reports: https://github.com/rzk-lang/rzk/issues
author: Nikolai Kudasov
maintainer: nickolay.kudasov@gmail.com
copyright: 2023-2025 Nikolai Kudasov
license: BSD3
license-file: LICENSE
build-type: Simple
extra-source-files:
grammar/Syntax.cf
test/typecheck/SCHEMA.md
test/typecheck/cases/happy-check.rzk
test/typecheck/cases/happy-flip-unflip.rzk
test/typecheck/cases/happy-interval-basics.rzk
test/typecheck/cases/happy-interval-subtyping.rzk
test/typecheck/cases/happy-issue-9-relfunext2-id.rzk
test/typecheck/cases/happy-modal-basics.rzk
test/typecheck/cases/happy-modal-flat-recOR-under-op.rzk
test/typecheck/cases/happy-modal-flat-under-op.rzk
test/typecheck/cases/happy-modal-inv.rzk
test/typecheck/cases/happy-modal-tope-unwrap.rzk
test/typecheck/cases/happy-modal-topes.rzk
test/typecheck/cases/happy-multivar-binder.rzk
test/typecheck/cases/happy-op-hom-to-hom.rzk
test/typecheck/cases/happy-recbot-term-wellformed.rzk
test/typecheck/cases/happy-recor-guard-exceeds-context.rzk
test/typecheck/cases/happy-recor-split-simplex-overhang.rzk
test/typecheck/cases/happy-refl-path.rzk
test/typecheck/cases/happy-restrict-face-not-contained.rzk
test/typecheck/cases/happy-shott-simplicial-subcomplexes.rzk
test/typecheck/cases/happy-tope-high-dim-cubes.rzk
test/typecheck/cases/happy-tope-nested-rec-or-d4.rzk
test/typecheck/cases/happy-tope-nested-rec-or-d5.rzk
test/typecheck/cases/happy-tope-nested-rec-or-d6.rzk
test/typecheck/cases/happy-tope-nested-rec-or.rzk
test/typecheck/cases/happy-tope-rec-and-restrict.rzk
test/typecheck/cases/happy-tope-shapes.rzk
test/typecheck/cases/ill-bare-lambda-compute.rzk
test/typecheck/cases/ill-bare-refl-compute.rzk
test/typecheck/cases/ill-duplicate.rzk
test/typecheck/cases/ill-hole-infer.rzk
test/typecheck/cases/ill-hole-pattern-binder-names.rzk
test/typecheck/cases/ill-hole-recor-branch.rzk
test/typecheck/cases/ill-hole-unsolved.rzk
test/typecheck/cases/ill-implicit.rzk
test/typecheck/cases/ill-interval-no-totality.rzk
test/typecheck/cases/ill-interval-subtyping.rzk
test/typecheck/cases/ill-invalid-arg-type-bot.rzk
test/typecheck/cases/ill-issue-13-flip-flip-wrong.rzk
test/typecheck/cases/ill-issue-206-families-of-extension.rzk
test/typecheck/cases/ill-issue-33-restriction-coherence.rzk
test/typecheck/cases/ill-modal-b-no-dist.rzk
test/typecheck/cases/ill-modal-flat-no-commute.rzk
test/typecheck/cases/ill-modal-not-modal.rzk
test/typecheck/cases/ill-modal-op-at-plain.rzk
test/typecheck/cases/ill-modal-op-under-flat.rzk
test/typecheck/cases/ill-modal-plain-under-flat.rzk
test/typecheck/cases/ill-modal-plain-under-op.rzk
test/typecheck/cases/ill-modal-recBOT-under-op-no-contradiction.rzk
test/typecheck/cases/ill-modal-sharp-at-plain.rzk
test/typecheck/cases/ill-modal-sharp-bot-not-bot.rzk
test/typecheck/cases/ill-modal-sharp-recOR-plain-var.rzk
test/typecheck/cases/ill-modal-sharp-under-flat.rzk
test/typecheck/cases/ill-modal-sharp-under-op.rzk
test/typecheck/cases/ill-modal-tope-cross-modality.rzk
test/typecheck/cases/ill-not-function.rzk
test/typecheck/cases/ill-not-pair-first-unit.rzk
test/typecheck/cases/ill-not-pair-second-unit.rzk
test/typecheck/cases/ill-param-untyped-pattern.rzk
test/typecheck/cases/ill-rec-or-overlap-incoherent.rzk
test/typecheck/cases/ill-recbot-term-not-function.rzk
test/typecheck/cases/ill-recbot-term-undefined.rzk
test/typecheck/cases/ill-recor-as-tope.rzk
test/typecheck/cases/ill-recor-coverage-required.rzk
test/typecheck/cases/ill-recor-guard-disjoint.rzk
test/typecheck/cases/ill-render-latex-define.rzk
test/typecheck/cases/ill-restrict-face-disjoint.rzk
test/typecheck/cases/ill-section-end-mismatch.rzk
test/typecheck/cases/ill-section-not-closed.rzk
test/typecheck/cases/ill-section-unexpected-end.rzk
test/typecheck/cases/ill-set-option-render.rzk
test/typecheck/cases/ill-set-option-unknown.rzk
test/typecheck/cases/ill-set-option-verbosity.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d4.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d5.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d6.rzk
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton.rzk
test/typecheck/cases/ill-tope-not-satisfied-app-shape.rzk
test/typecheck/cases/ill-tope-not-satisfied-rec-bot.rzk
test/typecheck/cases/ill-tope-not-satisfied-rec-or-boundary-equiv.rzk
test/typecheck/cases/ill-tope-not-satisfied-rec-or-open-singleton.rzk
test/typecheck/cases/ill-tope-not-satisfied-tope-family-subtyping.rzk
test/typecheck/cases/ill-tope-param-lambda.rzk
test/typecheck/cases/ill-tope-param-typefun.rzk
test/typecheck/cases/ill-tope-pattern-binder-bare.rzk
test/typecheck/cases/ill-tope-recOR-non-discrete.rzk
test/typecheck/cases/ill-tope-subtle-app-shape-5d.rzk
test/typecheck/cases/ill-tope-subtle-rec-or-5d-boundary.rzk
test/typecheck/cases/ill-tope-subtle-tope-family-4d.rzk
test/typecheck/cases/ill-tope-subtle-tope-family-5d.rzk
test/typecheck/cases/ill-undefined.rzk
test/typecheck/cases/ill-unexpected-lambda.rzk
test/typecheck/cases/ill-unexpected-pair.rzk
test/typecheck/cases/ill-unexpected-refl.rzk
test/typecheck/cases/ill-unify-terms-path.rzk
test/typecheck/cases/ill-unify.rzk
test/typecheck/cases/ill-unset-option-unknown.rzk
test/typecheck/cases/ill-unused-assumption.rzk
test/typecheck/cases/multimodule-first-error/bad.rzk
test/typecheck/cases/multimodule-first-error/lib.rzk
test/typecheck/cases/multimodule-two-ok/lib.rzk
test/typecheck/cases/multimodule-two-ok/user.rzk
test/typecheck/cases/uses-whnf-discarded.rzk
test/typecheck/cases/uses-whnf-masked-transitive.rzk
test/typecheck/cases/happy-check.expect.yaml
test/typecheck/cases/happy-flip-unflip.expect.yaml
test/typecheck/cases/happy-interval-basics.expect.yaml
test/typecheck/cases/happy-interval-subtyping.expect.yaml
test/typecheck/cases/happy-issue-9-relfunext2-id.expect.yaml
test/typecheck/cases/happy-modal-basics.expect.yaml
test/typecheck/cases/happy-modal-flat-recOR-under-op.expect.yaml
test/typecheck/cases/happy-modal-flat-under-op.expect.yaml
test/typecheck/cases/happy-modal-inv.expect.yaml
test/typecheck/cases/happy-modal-tope-unwrap.expect.yaml
test/typecheck/cases/happy-modal-topes.expect.yaml
test/typecheck/cases/happy-multivar-binder.expect.yaml
test/typecheck/cases/happy-op-hom-to-hom.expect.yaml
test/typecheck/cases/happy-recbot-term-wellformed.expect.yaml
test/typecheck/cases/happy-recor-guard-exceeds-context.expect.yaml
test/typecheck/cases/happy-recor-split-simplex-overhang.expect.yaml
test/typecheck/cases/happy-refl-path.expect.yaml
test/typecheck/cases/happy-restrict-face-not-contained.expect.yaml
test/typecheck/cases/happy-shott-simplicial-subcomplexes.expect.yaml
test/typecheck/cases/happy-tope-high-dim-cubes.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or-d4.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or-d5.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or-d6.expect.yaml
test/typecheck/cases/happy-tope-nested-rec-or.expect.yaml
test/typecheck/cases/happy-tope-rec-and-restrict.expect.yaml
test/typecheck/cases/happy-tope-shapes.expect.yaml
test/typecheck/cases/ill-bare-lambda-compute.expect.yaml
test/typecheck/cases/ill-bare-refl-compute.expect.yaml
test/typecheck/cases/ill-duplicate.expect.yaml
test/typecheck/cases/ill-hole-infer.expect.yaml
test/typecheck/cases/ill-hole-pattern-binder-names.expect.yaml
test/typecheck/cases/ill-hole-recor-branch.expect.yaml
test/typecheck/cases/ill-hole-unsolved.expect.yaml
test/typecheck/cases/ill-implicit.expect.yaml
test/typecheck/cases/ill-interval-no-totality.expect.yaml
test/typecheck/cases/ill-interval-subtyping.expect.yaml
test/typecheck/cases/ill-invalid-arg-type-bot.expect.yaml
test/typecheck/cases/ill-issue-13-flip-flip-wrong.expect.yaml
test/typecheck/cases/ill-issue-206-families-of-extension.expect.yaml
test/typecheck/cases/ill-issue-33-restriction-coherence.expect.yaml
test/typecheck/cases/ill-modal-b-no-dist.expect.yaml
test/typecheck/cases/ill-modal-flat-no-commute.expect.yaml
test/typecheck/cases/ill-modal-not-modal.expect.yaml
test/typecheck/cases/ill-modal-op-at-plain.expect.yaml
test/typecheck/cases/ill-modal-op-under-flat.expect.yaml
test/typecheck/cases/ill-modal-plain-under-flat.expect.yaml
test/typecheck/cases/ill-modal-plain-under-op.expect.yaml
test/typecheck/cases/ill-modal-recBOT-under-op-no-contradiction.expect.yaml
test/typecheck/cases/ill-modal-sharp-at-plain.expect.yaml
test/typecheck/cases/ill-modal-sharp-bot-not-bot.expect.yaml
test/typecheck/cases/ill-modal-sharp-recOR-plain-var.expect.yaml
test/typecheck/cases/ill-modal-sharp-under-flat.expect.yaml
test/typecheck/cases/ill-modal-sharp-under-op.expect.yaml
test/typecheck/cases/ill-modal-tope-cross-modality.expect.yaml
test/typecheck/cases/ill-not-function.expect.yaml
test/typecheck/cases/ill-not-pair-first-unit.expect.yaml
test/typecheck/cases/ill-not-pair-second-unit.expect.yaml
test/typecheck/cases/ill-param-untyped-pattern.expect.yaml
test/typecheck/cases/ill-rec-or-overlap-incoherent.expect.yaml
test/typecheck/cases/ill-recbot-term-not-function.expect.yaml
test/typecheck/cases/ill-recbot-term-undefined.expect.yaml
test/typecheck/cases/ill-recor-as-tope.expect.yaml
test/typecheck/cases/ill-recor-coverage-required.expect.yaml
test/typecheck/cases/ill-recor-guard-disjoint.expect.yaml
test/typecheck/cases/ill-render-latex-define.expect.yaml
test/typecheck/cases/ill-restrict-face-disjoint.expect.yaml
test/typecheck/cases/ill-section-end-mismatch.expect.yaml
test/typecheck/cases/ill-section-not-closed.expect.yaml
test/typecheck/cases/ill-section-unexpected-end.expect.yaml
test/typecheck/cases/ill-set-option-render.expect.yaml
test/typecheck/cases/ill-set-option-unknown.expect.yaml
test/typecheck/cases/ill-set-option-verbosity.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d4.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d5.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d6.expect.yaml
test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-app-shape.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-rec-bot.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-rec-or-boundary-equiv.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-rec-or-open-singleton.expect.yaml
test/typecheck/cases/ill-tope-not-satisfied-tope-family-subtyping.expect.yaml
test/typecheck/cases/ill-tope-param-lambda.expect.yaml
test/typecheck/cases/ill-tope-param-typefun.expect.yaml
test/typecheck/cases/ill-tope-pattern-binder-bare.expect.yaml
test/typecheck/cases/ill-tope-recOR-non-discrete.expect.yaml
test/typecheck/cases/ill-tope-subtle-app-shape-5d.expect.yaml
test/typecheck/cases/ill-tope-subtle-rec-or-5d-boundary.expect.yaml
test/typecheck/cases/ill-tope-subtle-tope-family-4d.expect.yaml
test/typecheck/cases/ill-tope-subtle-tope-family-5d.expect.yaml
test/typecheck/cases/ill-undefined.expect.yaml
test/typecheck/cases/ill-unexpected-lambda.expect.yaml
test/typecheck/cases/ill-unexpected-pair.expect.yaml
test/typecheck/cases/ill-unexpected-refl.expect.yaml
test/typecheck/cases/ill-unify-terms-path.expect.yaml
test/typecheck/cases/ill-unify.expect.yaml
test/typecheck/cases/ill-unset-option-unknown.expect.yaml
test/typecheck/cases/ill-unused-assumption.expect.yaml
test/typecheck/cases/uses-whnf-discarded.expect.yaml
test/typecheck/cases/uses-whnf-masked-transitive.expect.yaml
test/typecheck/cases/literate-fence/expect.yaml
test/typecheck/cases/multimodule-first-error/expect.yaml
test/typecheck/cases/multimodule-two-ok/expect.yaml
test/typecheck/cases/literate-fence/doc.rzk.md
extra-doc-files:
README.md
ChangeLog.md
source-repository head
type: git
location: https://github.com/rzk-lang/rzk
flag lsp
description: Build with LSP support (only available with GHC, not GHCJS).
manual: True
default: True
library
exposed-modules:
Free.Scoped
Free.Scoped.TH
Language.Rzk.Free.Syntax
Language.Rzk.Syntax
Language.Rzk.Syntax.Abs
Language.Rzk.Syntax.Layout
Language.Rzk.Syntax.Lex
Language.Rzk.Syntax.Par
Language.Rzk.Syntax.Print
Rzk
Rzk.Diagnostic
Rzk.Format
Rzk.Main
Rzk.Project.Config
Rzk.TypeCheck
other-modules:
Paths_rzk
autogen-modules:
Paths_rzk
hs-source-dirs:
src
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
build-depends:
Glob >=0.9.3 && <1
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.7 && <5
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, directory >=1.2.7.0 && <2
, mtl >=2.2.2 && <3
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED
if flag(lsp) && !impl(ghcjs)
exposed-modules:
Language.Rzk.VSCode.Config
Language.Rzk.VSCode.Env
Language.Rzk.VSCode.Handlers
Language.Rzk.VSCode.Logging
Language.Rzk.VSCode.Lsp
Language.Rzk.VSCode.Tokenize
build-depends:
aeson >=2.0.0.0 && <3
, co-log-core >=0.3.2.0 && <1
, data-default-class >=0.1.2.0 && <1
, filepath >=1.4.100.0 && <2
, lens >=5.0.1 && <6
, lsp >=2.4.0.0 && <3
, lsp-types >=2.1.1.0 && <3
, mtl >=2.3.1 && <3
, stm >=2.5.1.0 && <3
executable rzk
main-is: Main.hs
other-modules:
Paths_rzk
autogen-modules:
Paths_rzk
hs-source-dirs:
app
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
build-depends:
Glob >=0.9.3 && <1
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.7 && <5
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, directory >=1.2.7.0 && <2
, mtl >=2.2.2 && <3
, rzk
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED
if !impl(ghcjs)
build-depends:
optparse-generic >=1.4.7 && <2
, with-utf8 >=1.0.3.0 && <2
test-suite doctests
type: exitcode-stdio-1.0
main-is: doctests.hs
hs-source-dirs:
test
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
build-depends:
Glob >=0.9.3 && <1
, QuickCheck >=2.14 && <3
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.11.0.0 && <5.0
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, directory >=1.2.7.0 && <2
, doctest-parallel >=0.3 && <1
, mtl >=2.2.2 && <3
, rzk
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED
test-suite rzk-test
type: exitcode-stdio-1.0
main-is: Spec.hs
other-modules:
Rzk.DiagnosticSpec
Rzk.FormatSpec
Rzk.HolesSpec
Rzk.TypeCheckSpec
Paths_rzk
autogen-modules:
Paths_rzk
hs-source-dirs:
test
default-extensions:
DeriveDataTypeable
ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
build-tool-depends:
hspec-discover:hspec-discover >=2.7 && <3
build-depends:
Glob >=0.9.3 && <1
, aeson >=1.4 && <3
, array >=0.5.3.0 && <1
, base >=4.7 && <5
, bifunctors >=5.5.3 && <6
, bytestring >=0.10.8.2 && <1
, directory >=1.2.7.0 && <2
, filepath >=1.4 && <2
, hspec >=2.7 && <3
, hspec-discover >=2.7 && <3
, mtl >=2.2.2 && <3
, rzk
, template-haskell >=2.14.0.0 && <3
, text >=1.2.3.1 && <3
, yaml >=0.11.0.0 && <1
default-language: Haskell2010
if flag(lsp) && !impl(ghcjs)
cpp-options: -DLSP_ENABLED