Updates and improvements

.github/workflows/flake-build.yml

@@ -0,0 +1,29 @@
+name: Flake build
+permissions: read-all
+concurrency:
+  cancel-in-progress: true
+  group: ${{ github.actor }}
+
+# Controls when the action will run.
+on:
+  # Triggers the workflow on push or pull request events but only for the master branch
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+jobs:
+  # This workflow contains a single job called "build"
+  build:
+    # The type of runner that the job will run on
+    runs-on: ubuntu-latest
+
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+    - uses: actions/checkout@v4
+    - uses: docker://ghcr.io/fluidattacks/makes/amd64:24.02
+      with:
+        args: sh -c "chown -R root:root /github/workspace && m . /build"

.gitignore

@@ -38,3 +38,7 @@ _opam/
 _objects/
 .nia.cache
 .lia.cache
+/.direnv/
+/.envrc
+result*
+/coq.kernel

CITATION.cff

@@ -0,0 +1,49 @@
+# This CITATION.cff file was generated with cffinit.
+# Visit https://bit.ly/cffinit to generate yours today!
+
+cff-version: 1.2.0
+title: 'Kôika: A Core Language for Rule-Based Hardware Design'
+message: >-
+  If you use this software, please cite it using the
+  metadata from this file.
+type: software
+authors:
+  - given-names: Clément
+    family-names: Pit-Claudel
+    orcid: 'https://orcid.org/0000-0002-1900-3901'
+  - given-names: Mathieu
+    family-names: Fehr
+    orcid: 'https://orcid.org/0000-0002-4100-3190'
+identifiers:
+  - type: doi
+    value: 10.1145/3385412.3385965
+    description: The ACM deposit of the encompassing paper.
+repository-code: 'https://github.com/mit-plv/koika'
+repository: 'https://github.com/mit-plv/koika'
+abstract: >-
+  Rule-based hardware design language and verified compiler.
+  The compiler is implemented in the Coq System and OCaml.
+  The DSL is embedded in Coq and provides one-rule-at-a-time
+  (ORAAT) descriptive semantics to implement stateful
+  hardware on the register transfer level.
+keywords:
+  - Hardware Description Language
+  - Formal Verification
+  - Verilog
+  - Compiler
+license: GPL-3.0
+preferred-citation:
+  type: article
+  title: 'The essence of Bluespec: a core language for rule-based hardware design'
+  authors:
+    - family-names: Bourgeat
+      given-names: Thomas
+      orcid: 'https://orcid.org/0000-0002-8468-8409'
+    - family-names: Pit-Claudel
+      given-names: Clément
+      orcid: 'https://orcid.org/0000-0002-1900-3901'
+    - family-names: Chlipala
+      given-names: Adam
+    - given-names: Arvind
+  year: 2020
+  doi: 10.1145/3385412.3385965

CONTRIBUTING.md

@@ -0,0 +1,31 @@
+# Contributing to Kôika
+
+To start contributing, you need a GitHub account and create a pull-request against this repository.
+See [here](https://docs.github.com/en/get-started/quickstart/hello-world) for a primer.
+
+# How to do
+
+## Before submitting a pull request
+
+Run the tests to check if your changes broke anything.
+You will do everyone the biggest favour if you run the continuous integration runner to build and test Kôika.
+This assumes that you have the [Nix](https://nixos.org/download) Package Manager installed with the support for flakes enabled.
+Suppose Nix is set up correctly, you just run:
+
+```sh
+nix run .#makes -- . /build
+```
+
+## Locally reproduce a CI run
+
+Suppose you want to produce a CI run locally, maybe because it has failed on GitHub or because you want to run it on a different commit of a pull request that consist of multiple commits.
+You can adapt the previously shown call to `makes` to do that; replace `<rev>` with the commit hash of interest:
+
+```sh
+# use the commit directly from GitHub
+nix run .#makes -- github:Barkhausen-Institut/koika@<rev> /build
+# alternatively, if the commit is already locally available
+nix run .#makes -- local:"$PWD"@<rev> /build
+```
+
+If necessary, `makes` downloads the repository in the state given in `<rev>` and executes the CI script referenced via `/build`.

Makefile

@@ -14,8 +14,8 @@ endif
 
 OBJ_DIR := _obj
 BUILD_DIR := _build/default
-COQ_BUILD_DIR := ${BUILD_DIR}/coq
-OCAML_BUILD_DIR := ${BUILD_DIR}/ocaml
+COQ_BUILD_DIR := $(BUILD_DIR)/coq
+OCAML_BUILD_DIR := $(BUILD_DIR)/ocaml
 
 V ?=
 verbose := $(if $(V),,@)
@@ -60,69 +60,61 @@ ocaml:
 # and eval because patterns like ‘%1/_objects/%2.v/: %1/%2.v’ aren't supported.
 # https://www.gnu.org/software/make/manual/html_node/Canned-Recipes.html
 # https://www.gnu.org/software/make/manual/html_node/Eval-Function.html
-
-target_directory = $(dir $(1))_objects/$(notdir $(1))
+#
+# This code is not very useful anymore, because everything, including selecting
+# which examples/tests are to be built, is done in examples/dune and tests/dune,
+# now.  The code is left here, because the dune code does not support .etc
+# supplements, yet, and to give make the right™ targets for examples/tests.
+# This means that the assignments to TESTS and EXAMPLES must be kept in sync
+# with their respective dune files!
+
+target_directory = $(1).d
 target_directories = $(foreach fname,$(1),$(call target_directory,$(fname)))
 
-define cuttlec_recipe_prelude =
-	@printf "\n-- Compiling %s --\n" "$<"
-endef
-
 # Execute follow-ups if any
 define cuttlec_recipe_coda =
-	$(verbose)if [ -d $<.etc ]; then cp -rf $<.etc/. "$@"; fi
-	$(verbose)if [ -d $(dir $<)etc ]; then cp -rf $(dir $<)etc/. "$@"; fi
-	$(verbose)if [ -f "$@/Makefile" ]; then $(MAKE) -C "$@"; fi
+	$(verbose)if [ -d $<.etc ]; then cp -rf $<.etc/. "$(BUILD_DIR)$@"; fi
+	$(verbose)if [ -d $(dir $<)etc ]; then cp -rf $(dir $<)etc/. "$(BUILD_DIR)$@"; fi
+	$(verbose)if [ -f "$(BUILD_DIR)$@/Makefile" ]; then $(MAKE) -C "$(BUILD_DIR)$@"; fi
 endef
 
-# Compile a .lv file
-define cuttlec_lv_recipe_body =
-	dune exec -- cuttlec "$<" \
-		-T all -o "$@" $(if $(findstring .1.,$<),--expect-errors 2> "$@stderr")
-endef
-
-# Compile a .v file
-define cuttlec_v_recipe_body =
-	dune build "$@/$(notdir $(<:.v=.ml))"
-	dune exec -- cuttlec "${BUILD_DIR}/$@/$(notdir $(<:.v=.ml))" -T all -o "$@"
-endef
-
-define cuttlec_lv_template =
-$(eval dirpath := $(call target_directory,$(1)))
-$(dirpath) $(dirpath)/: $(1) ocaml | configure
-	$(value cuttlec_recipe_prelude)
-	$(value cuttlec_lv_recipe_body)
-	$(value cuttlec_recipe_coda)
+define cuttlec_recipe =
+	@printf "\n-- Compiling %s --\n" "$<"
+	dune build "@$@/runtest"
 endef
 
-define cuttlec_v_template =
+define cuttlec_template =
 $(eval dirpath := $(call target_directory,$(1)))
-$(dirpath) $(dirpath)/: $(1) ocaml | configure
-	$(value cuttlec_recipe_prelude)
-	$(value cuttlec_v_recipe_body)
+$(dirpath) $(dirpath)/: $(1)
+	$(value cuttlec_recipe)
 	$(value cuttlec_recipe_coda)
 endef
 
 TESTS := $(wildcard tests/*.lv) $(wildcard tests/*.v)
 EXAMPLES := $(wildcard examples/*.lv) $(wildcard examples/*.v) examples/rv/rv32i.v examples/rv/rv32e.v
 
-configure:
-	etc/configure $(filter %.v,${TESTS} ${EXAMPLES})
+$(foreach fname,$(EXAMPLES) $(TESTS),\
+	$(eval $(call cuttlec_template,$(fname))))
 
-$(foreach fname,$(filter %.lv, $(EXAMPLES) $(TESTS)),\
-	$(eval $(call cuttlec_lv_template,$(fname))))
-$(foreach fname,$(filter %.v, $(EXAMPLES) $(TESTS)),\
-	$(eval $(call cuttlec_v_template,$(fname))))
+examples: coq.kernel
+	dune build @examples/runtest
 
-examples: $(call target_directories,$(EXAMPLES));
 clean-examples:
-	find examples/ -type d \( -name _objects -or -name _build \) -exec rm -rf {} +
-	rm -rf ${BUILD_DIR}/examples
+	find examples/ -type d \( -name '*.d' \) -exec rm -rf {} +
+	rm -rf $(BUILD_DIR)/examples
+
+tests:
+	dune build @tests/runtest
 
-tests: $(call target_directories,$(TESTS));
 clean-tests:
-	find tests/ -type d  \( -name _objects -or -name _build \) -exec rm -rf {} +
-	rm -rf ${BUILD_DIR}/tests
+	find tests/ -type d  \( -name '*.d' \) -exec rm -rf {} +
+	rm -rf $(BUILD_DIR)/tests
+
+# HACK: Part One of a two-part hack. When using nix, dune does not provide the
+# OCaml libs of Coq to its targets. Thus, link the libs to a well-known location
+# and add specific "-nI" include flags in e.g. examples/rv/dune.
+coq.kernel:
+	@./coq.kernel.hack.sh
 
 .PHONY: configure examples clean-examples tests clean-tests
 
@@ -144,7 +136,7 @@ all: coq ocaml examples tests readme;
 
 clean: clean-tests clean-examples
 	dune clean
-	rm -f koika-*.tar.gz
+	rm -f koika-*.tar.gz coq.kernel
 
 .PHONY: readme package dune-all all clean
 

README.rst

@@ -16,53 +16,52 @@ Our largest example at the moment is a simple RISCV (RV32I) `4-stage pipelined c
 
 This README provides practical information to get started with Kôika.  For details about Kôika's semantics, its compilation algorithm, and the work it draws inspiration from, please read our PLDI 2020 paper: `The Essence of Bluespec, A Core Language for Rule-Based Hardware Design <https://dl.acm.org/doi/10.1145/3385412.3385965>`_.
 
-.. raw:: html
-
-   <a href="https://github.com/mit-plv/koika/">
-     <img src="https://raw.githubusercontent.com/mit-plv/koika/master/etc/logo/cover.jpg" align="center" />
-   </a>
+.. image:: etc/logo/cover.jpg
+           :alt: Kôika logo showing a cuttlefish
+           :target: https://github.com/mit-plv/koika/
 
 Getting started
 ===============
 
 Installing dependencies and building from source
 ------------------------------------------------
 
-* OCaml 4.07 through 4.09, `opam <https://opam.ocaml.org/doc/Install.html>`_ 2.0 or later, GNU make.
+* OCaml 4.14 `opam <https://opam.ocaml.org/doc/Install.html>`_ 2.0 or later, GNU make.
 
-* Coq 8.11 through 8.13::
+* Coq 8.18::
 
-    opam install coq=8.12.2
+    opam install coq=8.18
 
-* Dune 2.5 or later::
+* Dune 3.14 or later::
 
     opam upgrade dune
 
 * Some OCaml packages::
 
-    opam install base core stdio parsexp hashcons zarith
+    opam install base core core_unix stdio parsexp hashcons zarith
 
 * To run the tests of our RISCV core, a `RISCV compilation toolchain <https://github.com/xpack-dev-tools/riscv-none-embed-gcc-xpack/releases/>`_.
 
 * To run C++ simulations: a recent C++ compiler (clang or gcc), ``libboost-dev``, and optionally ``clang-format``.
 
-You can compile the full distribution, including examples, tests, and proofs by running ``make`` in the top-level directory of this repo.  Generated files are placed in ``_build``, ``examples/_objects/``,  ``tests/_objects/``, and  ``examples/rv/_objects/``.
+* To compile this README, you need ``sphinx`` and its tool ``rst2html5``.
+
+You can compile the full distribution, including examples, tests, and proofs by running ``dune build @runtest`` in the top-level directory of this repo.  Generated files are placed in ``_build``.
 
-Each directory in ``_objects`` contains `a Makefile <makefile_>`_ to ease further experimentation (including RTL simulation, profiling, trace generation, etc.).
+.. Each directory in ``_objects`` contains `a Makefile <makefile_>`_ to ease further experimentation (including RTL simulation, profiling, trace generation, etc.).
 
 .. opam show -f name,version coq dune base core stdio parsexp hashcons zarith | sed 's/name *//' | tr '\n' ' ' | sed 's/ *version */=/g' | xclip
 
 For reproducibility, here is one set of versions known to work:
 
-- OCaml 4.09 with ``opam install base=v0.13.1 coq=8.11.1 core=v0.13.0 dune=2.5.1 hashcons=1.3 parsexp=v0.13.0 stdio=v0.13.0 zarith=1.9.1``
+- OCaml 4.14.2 with ``opam install base=v0.16.2 coq=8.18 core=v0.16.2 dune=3.15.1 hashcons=1.4 parsexp=v0.16.0 stdio=v0.16.0 zarith=1.13``
+
+- Additionally, we provide a ``flake.nix`` file that allows you to download, install and use a working set of programs by just calling ``nix develop`` (provided, that you have Nix installed. See also the `Nix Package Manager <https://nixos.org/download>`_).
 
 Browsing examples
 -----------------
 
-The ``examples/`` directory of this repo demonstrates many of |koika|'s features.
-The examples can be compiled using ``make examples``, and browsed in either
-CoqIDE or Proof General.  There is basic Emacs support for ``.lv`` files (the “Lispy
-Verilog” alternative frontend for |koika|) in ``etc/lv-mode.el``.
+The ``examples/`` directory of this repo demonstrates many of |koika|'s features.  The examples can be compiled using ``dune build @examples/runtest``, and browsed in either CoqIDE or Proof General.  There is basic Emacs support for ``.lv`` files (the “Lispy Verilog” alternative frontend for |koika|) in ``etc/lv-mode.el``.
 
 See `browsing the sources <repo-map_>`_ below for information about the repository's organization.
 
@@ -78,7 +77,10 @@ Our compiler (``cuttlec``) supports multiple targets:
 - ``makefile`` (an auto-generated Makefile including convenient targets to debug, profile, trace, or visualize the outputs of your design)
 - ``dot`` (a basic representation of the RTL generated from your design)
 
-For quick experimentation, you can just drop your files in ``examples/`` or ``tests/`` and run ``make examples/_objects/<your-file.v>/``.
+For quick experimentation, you can just drop your files in ``examples/`` and run:
+
+- ``dune build @examples/genrules`` (only needs to be done once for every new file) followed by
+- ``dune build @examples/<your-file.v>.d/runtest``.
 
 Programs written in the Coq EDSL
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -139,6 +141,7 @@ The semantics of |koika| guarantee that each rule executes atomically, and that
 As an example, consider a simple two-stage pipeline with two single-element input FIFOs and one single-element output FIFO:
 
 .. image:: etc/readme/pipeline.svg
+           :alt: A diagram with two input FIFOs on the left feeding into a register stage that is read by a "process". The result is written to the next register stage that feeds the output FIFO.
 
 We implement these FIFOs using three single-bit registers (``…_empty``) indicating whether each FIFO is empty, and three data registers (``…_data``) holding the contents of these FIFOs.  We have three rules: two to dequeue from the input FIFOs into a middle FIFO (``deq0`` and ``deq1``), and one to dequeue from the middle FIFO and write a result (the input plus 412) into an output FIFO (``process``).  The code looks like this (``guard(condition)`` is short for ``if !condition then fail``):
 

coq.kernel.hack.sh

@@ -0,0 +1,3 @@
+#!/bin/sh
+rm -f coq.kernel
+ln -s $(find -L $(coqc --config | sed -n -E -e '/^COQLIB=/s;^COQLIB=(.*)/coq;\1/ocaml;p') -type d -name kernel) coq.kernel