Carnap is a free and open-source Haskell framework for creating and exploring formal languages, logics, and semantics. It lets you quickly and straightforwardly define languages, construct logics for those languages, and stipulate their semantics. Carnap then uses your specifications to figure out how to check proofs in a variety of formal systems using your logic, how to find the meanings of compound expressions, and a whole lot more.
Carnap's primary application at the moment is powering Carnap.io, a website supporting online logic instruction and learning. If you'd like to see some demos and more general information, head over to Carnap.io/about.
If you'd like to learn more about using the server as an instructor, head over to the documentation collection.. You can also find documentation about administration-focused topics such as deployment and server configuration there. Documentation is updated nightly from the Carnap-Documentation repository, in case you'd like to contribute or suggest an edit.
If you'd like to discuss development and administration of Carnap instances in real time, we have a chat room on Matrix, bridged to libera.chat in #carnap.
There is also a mailing list, primarily focused on instructor support, on Google Groups.
If you're interested in contributing to software development or modifying the software, read on. This README will help you set up a development environment for building the server-side and client-side components used on carnap.io.
The current development environment is based on Nix. For general background on Nix, take a look at nixos.org/learn.html or nix.dev.
The Nix package manager runs on any Linux distribution or macOS and can be installed without disrupting the rest of your system.
Building on Windows natively is not supported, however, Carnap works well in the Windows Subsystem for Linux, and has been tested and confirmed working in WSL 2. The steps for Linux work as-written in WSL 2.
Nix is used to speed up builds and avoid having to compile dependencies, instead using cached built versions from the NixOS build farm. It also makes it easy to build lean Docker images and implement CI.
Carnap has a GHCJS (client side) and a GHC (server side) part.
Nix does not support incremental package builds, so the suggested development
workflow is to use the standard Haskell build system cabal in a nix-shell.
A Makefile has been provided to make this easier by shortening the commands
needed to be typed. It will output the commands it runs, and you can also read
the Makefile itself for more details.
In this documentation, lines starting with $ mean that the part after the $
is run in a shell natively on your system. Lines starting with [nix-shell]$
are intended to be run in a nix-shell shell, which will have that prompt.
Install Nix with your non-root user account:
$ bash <(curl -L https://nixos.org/nix/install)
macOS 10.15 (Catalina) users may need to follow additional steps, documented at nixos.org/nix/manual/#sect-macos-installation.
You can significantly speed up builds by using binaries for Carnap dependencies from Carnap's Cachix instance, which has support for both Linux and macOS. To use it:
$ # Install Cachix:
$ nix-env -iA cachix -f https://cachix.org/api/v1/install
$ # Use the Carnap Cachix
$ cachix use carnap
Then build as normal.
A quick aside (for those who are curious about what these commands are doing):
Nix, by default, reads shell.nix if you call it through nix-shell, and
default.nix if you call it with nix-build or others. That's why there are
attribute names being used with -A for the nix-build commands, but not for
nix-shell.
This creates a shell in an environment providing the required dependencies for
Carnap-Server, along with development tools such as cabal, ghc and others
appropriate for server side development. Nix shells use versions of Haskell
components and tools isolated from those available on the host system, sort of
like Python's virtualenv, but for Haskell packages, and in fact, the entire
machine.
$ nix-shell
[nix-shell:Carnap]$ # Run a development server
[nix-shell:Carnap]$ make run
You should then be able to access your development server at
http://localhost:3000.
To become an instructor, log in with the dummy login using an email you'll remember. Set your first name and last name. Then, go to http://localhost:3000/admin_promote and press the button. Your account will be promoted to administrator of the local instance.
From there, you can go to http://localhost:3000/master_admin and promote your account to instructor. You can log out and log back in with another email if you want to simulate a student, for example.
If you'd like to dig into the code, Haskell Language Server is highly recommended.
This process will replace the symlink to the Nix-built client automatically
built while working on the server with one to a cabal-built client, more
suitable for development. You can delete client-out and make run will give
you a Nix-built client again.
You can get a shell with a ghcjs compiler like so:
$ make shell-ghcjs
$ # This will invoke cabal to build the GHCJS components
[nix-shell:Carnap]$ make build-ghcjsThe truth tree components are built by Nix as well, in a nearly identical way to the client. If you'd like to replace them with a locally built one, replace the symlink with one pointing to a local checkout that's been built:
Say, you have a checkout of the repo
at ~/dev/Rudolf that you've already run yarn install and yarn build-lib
in, you'd want to run, in your Carnap directory:
Carnap$ ln -sfn ~/dev/Rudolf ./truth-tree-outIf you'd like to go back to the Nix-built truth tree, just delete the
truth-tree-out symlink.
If you'd like to build a release build of the Nix package, suitable for production, use:
$ nix-build -A server -o server-outThis builds the derivation at the attribute server of the attribute set
returned by the function at the top level of default.nix. You can also invoke
this function yourself if you want to use Carnap in a NixOps deployment, for
example:
let carnap-server = (import ./carnap/default.nix {}).server;
in {
# use it
# ...
}Here's a sample of NixOps files using this for a deployment of Carnap at UBC
If you'd like to build an image locally for development/testing, run:
$ nix-build release.nix -A docker -o docker-out
then load it into the docker daemon with:
$ docker image load -i docker-out
It will be available under the image name carnap:latest.
The docker building setup does not require KVM support in the host kernel, and
if you wish to build your images on a machine without it, run nix-build with
the added argument --arg hasKvm false.
The Nix infrastructure for Carnap provides the Haskell Language Server by default for development on Carnap-Server, allowing for completion, type information and more. It is not yet working on the exclusively-GHCJS-built components.
To use it:
Make the following shell script somewhere in $PATH, called hls-nix:
#!/bin/sh
nix-shell --run "haskell-language-server-wrapper $@"Then, configure per the information in the
README. For example, for
neovim with Coc, the following configuration should be put in the file
brought up by :CocConfig:
{
"languageserver": {
"haskell": {
"command": "hls-nix",
"args": ["--lsp"],
"rootPatterns": ["*.cabal", "stack.yaml", "cabal.project", "package.yaml", "hie.yaml"],
"filetypes": ["haskell", "lhaskell"]
}
}
}NOTE: we are using the hls-nix wrapper script as the command here, so HLS
picks up the dependencies for Carnap-Server from Nix since it is run in a
nix-shell.
NOTE: Carnap-Server/config/settings.yml needs to be present for Carnap-Server to
work in HLS (just copy it from the example settings file).
The documentation is available using the /srv/ route, which can also be used
locally. If you want to do this, you can make a symbolic link like the following:
carnap$ ln -s /path/to/your/clone/of/Carnap-Documentation ./dataroot/srv
You can then browse to http://localhost:3000/srv to have an immediate preview
of the documentation as you work on it.
CI requires that a Cachix signing key for the Cachix cache be supplied in the
CACHIX_SIGNING_KEY Secret in the GitHub repository settings for artifacts to
be pushed to Cachix.
The version of nixpkgs used is pinned to a fixed git commit to ensure that no
unexpected issues happen with our builds. Occasionally it should be updated,
then Carnap build reattempted. Currently we use a system of two versions of
nixpkgs, nixpkgs and nixpkgs-stable, with nixpkgs used for Carnap-Server,
having the latest packages including haskell-language-server, and
nixpkgs-stable providing a working ghcjs (since it is supposedly broken in
the latest nixpkgs). nixpkgs-stable as of the time of this writing is pinned
to nixos-20.03 whereas nixpkgs is on nixpkgs-unstable, a
tested-but-rolling-release build.
We now use niv to manage our nixpkgs versions. It is available from either development shell.
Run niv update nixpkgs or niv update nixpkgs-stable to update the
respective pinned nixpkgs versions to the latest in their branch.
Every instance of doJailbreak is disabling version checking in Cabal. Most of
the time this works fine, but it indicates bugs in the packages' Cabal
version restrictions.
Carnap currently uses an older ghcjs-dom from 2016, which is largely fine on web but requires webkitgtk24x-gtk3, which was been removed from Nix in late 2019. It is thus currently not possible to build the Carnap front end natively (i.e. for embedding in non-browser applications) pending this update.
A bunch of packages have broken unit tests on ghcjs. All tests on ghcjs are accordingly disabled (also, for performance reasons).
Blog post on Carnap's nix implementation: https://lfcode.ca/blog/nix-and-haskell
Tutorial some of the Nix here is loosely based on: https://github.com/Gabriel439/haskell-nix
User's guide to the Haskell infrastructure: https://nixos.org/nixpkgs/manual/#users-guide-to-the-haskell-infrastructure
Source code to the Haskell infrastructure (has good doc comments): https://github.com/NixOS/nixpkgs/tree/nixos-20.03/pkgs/development/haskell-modules
Basic information about the builder and e.g. how to build manually: https://nixos.wiki/wiki/Nixpkgs/Create_and_debug_packages