From 7f3ad4c156dad602481994b01f874bdb88b0b3f9 Mon Sep 17 00:00:00 2001 From: Michael Raitza Date: Thu, 16 May 2024 18:07:17 +0200 Subject: [PATCH] Modernise tool chain The Make-based tool chain is largely replaced by Dune, including rule generation for examples/tests. The make file relies on dune for most of its work. Filtering examples/tests is kept for convenience. Right now, .etc post-processing (to synthesise or simulate a model via the cuttlec Make-based tool chain) is dysfunctional. --- Makefile | 86 ++++------ coq.kernel.hack.sh | 3 + dune | 2 + etc/configure | 78 --------- etc/dune.lv.template | 0 etc/dune.v.template | 10 -- examples/dune | 211 +---------------------- examples/dune.inc | 333 +++++++++++++++++++++++++++++++++++++ examples/rv/dune | 32 +--- examples/rv/dune.inc | 38 +++++ flake.nix | 7 +- ruleGen.ml | 72 ++++++++ tests/dune | 176 +------------------- tests/dune.inc | 386 +++++++++++++++++++++++++++++++++++++++++++ 14 files changed, 891 insertions(+), 543 deletions(-) create mode 100755 coq.kernel.hack.sh delete mode 100755 etc/configure delete mode 100644 etc/dune.lv.template delete mode 100644 etc/dune.v.template create mode 100644 examples/dune.inc create mode 100644 examples/rv/dune.inc create mode 100644 ruleGen.ml create mode 100644 tests/dune.inc diff --git a/Makefile b/Makefile index 6f27d0da..e06ba227 100644 --- a/Makefile +++ b/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,76 +60,62 @@ 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 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 -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) +cuttlec_recipe_code = +# define cuttlec_recipe_coda = +# $(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 + +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: coq.kernel $(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. 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: - @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.hack.sh .PHONY: configure examples clean-examples tests clean-tests diff --git a/coq.kernel.hack.sh b/coq.kernel.hack.sh new file mode 100755 index 00000000..d2c4412c --- /dev/null +++ b/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 diff --git a/dune b/dune index 7d8ceba7..1d799900 100644 --- a/dune +++ b/dune @@ -3,3 +3,5 @@ (env (dev (flags (:standard -warn-error -A \ -short-paths)))) + +(executable (name ruleGen)) diff --git a/etc/configure b/etc/configure deleted file mode 100755 index 92d2f985..00000000 --- a/etc/configure +++ /dev/null @@ -1,78 +0,0 @@ -#!/usr/bin/env python3 -## Generate dune files for examples/ and tests/ - -import sys -from os import path, makedirs -from subprocess import check_call - -SCRIPT_DIR = path.dirname(path.realpath(__file__)) -SEPARATOR = "\n;; --- DO NOT EDIT BELOW THIS LINE (use ‘make configure’) ---\n" - -# def hardlink(src, dst): -# src, dst = path.join(path.normpath(src), "."), path.normpath(dst) -# if path.isdir(src): -# print("{} → {}".format(src, dst)) -# check_call(["cp", "--force", "--recursive", src, "-t", dst]) - -# def prepare_assets(dirpath, fname, objdir): -# makedirs(objdir, exist_ok=True) -# hardlink(path.join(dirpath, "etc"), objdir) -# hardlink(path.join(dirpath, fname + ".etc"), objdir) - -def gen_subdirs(dirpath, theory, templates, fnames): - """Format a single dune ``subdir`` stanza for a given `file`.""" - for fname in fnames: - objdir = path.join(dirpath, "_objects", fname) - module_name, fext = path.splitext(fname) - # prepare_assets(dirpath, fname, objdir) - makedirs(objdir, exist_ok=True) - yield templates[fext].format_map({ - "objdir": objdir, - "module_name": module_name, - "theory": theory }) - -def dune_contents(dune_path): - try: - with open(dune_path) as f: - contents = f.read() - endpos = contents.find(SEPARATOR) - return contents[:endpos] if endpos >= 0 else contents - except FileNotFoundError: - return "" - -# Included files cannot contain ‘subdir’ forms, so modify ‘dune’ in place -def gen_dune(templates, dirpath, fnames): - """Create a ``dune.inc`` file in `dirpath` covering all `fnames`.""" - theory = path.basename(dirpath) - forms = gen_subdirs(dirpath, theory, templates, fnames) - dune = path.join(dirpath, "dune") - contents = dune_contents(dune) - with open(dune, mode="w") as dunefile: - dunefile.write(contents) - dunefile.write(SEPARATOR) - dunefile.write("(dirs :standard _objects)\n") - for form in forms: - dunefile.write("\n\n" + form) - -def fread(fname): - with open(path.join(SCRIPT_DIR, fname)) as fl: - return fl.read() - -def gen_objdirs(files): - """Generate ``dune.inc`` files for all files in `files`.""" - files = sorted(files) - - templates = {} - for ext in (".v", ".lv"): - templates[ext] = fread("dune{}.template".format(ext)) - - by_directory = {} - for fpath in files: - dirpath, fname = path.split(fpath) - by_directory.setdefault(dirpath, []).append(fname) - - for dirpath, fnames in by_directory.items(): - gen_dune(templates, dirpath, fnames) - -if __name__ == '__main__': - gen_objdirs(sys.argv[1:]) diff --git a/etc/dune.lv.template b/etc/dune.lv.template deleted file mode 100644 index e69de29b..00000000 diff --git a/etc/dune.v.template b/etc/dune.v.template deleted file mode 100644 index f9171348..00000000 --- a/etc/dune.v.template +++ /dev/null @@ -1,10 +0,0 @@ -;; -*- dune -*- -(subdir "_objects/{module_name}.v" - (rule (write-file "{module_name}_extr.v" - "Require Coq.extraction.Extraction {theory}.{module_name}. -Extraction \"{module_name}.ml\" {module_name}.prog.")) - (coq.extraction - (prelude {module_name}_extr) - (extracted_modules {module_name}) - (theories Ltac2 Koika {theory}) - (flags "-w" "-overriding-logical-loadpath"))) diff --git a/examples/dune b/examples/dune index fc9aee1c..948c1b15 100644 --- a/examples/dune +++ b/examples/dune @@ -7,209 +7,10 @@ (env (dev (flags (:standard -w -39)))) -;; --- DO NOT EDIT BELOW THIS LINE (use ‘make configure’) --- -(dirs :standard _objects) +(include dune.inc) - -;; -*- dune -*- -(subdir "_objects/collatz.v" - (rule (write-file "collatz_extr.v" - "Require Coq.extraction.Extraction examples.collatz. -Extraction \"collatz.ml\" collatz.prog.")) - (coq.extraction - (prelude collatz_extr) - (extracted_modules collatz) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/combinational_proof_tutorial.v" - (rule (write-file "combinational_proof_tutorial_extr.v" - "Require Coq.extraction.Extraction examples.combinational_proof_tutorial. -Extraction \"combinational_proof_tutorial.ml\" combinational_proof_tutorial.prog.")) - (coq.extraction - (prelude combinational_proof_tutorial_extr) - (extracted_modules combinational_proof_tutorial) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/conflicts.v" - (rule (write-file "conflicts_extr.v" - "Require Coq.extraction.Extraction examples.conflicts. -Extraction \"conflicts.ml\" conflicts.prog.")) - (coq.extraction - (prelude conflicts_extr) - (extracted_modules conflicts) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/conflicts_modular.v" - (rule (write-file "conflicts_modular_extr.v" - "Require Coq.extraction.Extraction examples.conflicts_modular. -Extraction \"conflicts_modular.ml\" conflicts_modular.prog.")) - (coq.extraction - (prelude conflicts_modular_extr) - (extracted_modules conflicts_modular) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/cosimulation.v" - (rule (write-file "cosimulation_extr.v" - "Require Coq.extraction.Extraction examples.cosimulation. -Extraction \"cosimulation.ml\" cosimulation.prog.")) - (coq.extraction - (prelude cosimulation_extr) - (extracted_modules cosimulation) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/datatypes.v" - (rule (write-file "datatypes_extr.v" - "Require Coq.extraction.Extraction examples.datatypes. -Extraction \"datatypes.ml\" datatypes.prog.")) - (coq.extraction - (prelude datatypes_extr) - (extracted_modules datatypes) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/external_rule.v" - (rule (write-file "external_rule_extr.v" - "Require Coq.extraction.Extraction examples.external_rule. -Extraction \"external_rule.ml\" external_rule.prog.")) - (coq.extraction - (prelude external_rule_extr) - (extracted_modules external_rule) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/fft.v" - (rule (write-file "fft_extr.v" - "Require Coq.extraction.Extraction examples.fft. -Extraction \"fft.ml\" fft.prog.")) - (coq.extraction - (prelude fft_extr) - (extracted_modules fft) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/fir.v" - (rule (write-file "fir_extr.v" - "Require Coq.extraction.Extraction examples.fir. -Extraction \"fir.ml\" fir.prog.")) - (coq.extraction - (prelude fir_extr) - (extracted_modules fir) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/function_call.v" - (rule (write-file "function_call_extr.v" - "Require Coq.extraction.Extraction examples.function_call. -Extraction \"function_call.ml\" function_call.prog.")) - (coq.extraction - (prelude function_call_extr) - (extracted_modules function_call) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/gcd_machine.v" - (rule (write-file "gcd_machine_extr.v" - "Require Coq.extraction.Extraction examples.gcd_machine. -Extraction \"gcd_machine.ml\" gcd_machine.prog.")) - (coq.extraction - (prelude gcd_machine_extr) - (extracted_modules gcd_machine) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/method_call.v" - (rule (write-file "method_call_extr.v" - "Require Coq.extraction.Extraction examples.method_call. -Extraction \"method_call.ml\" method_call.prog.")) - (coq.extraction - (prelude method_call_extr) - (extracted_modules method_call) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/pipeline.v" - (rule (write-file "pipeline_extr.v" - "Require Coq.extraction.Extraction examples.pipeline. -Extraction \"pipeline.ml\" pipeline.prog.")) - (coq.extraction - (prelude pipeline_extr) - (extracted_modules pipeline) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/pipeline_tutorial.v" - (rule (write-file "pipeline_tutorial_extr.v" - "Require Coq.extraction.Extraction examples.pipeline_tutorial. -Extraction \"pipeline_tutorial.ml\" pipeline_tutorial.prog.")) - (coq.extraction - (prelude pipeline_tutorial_extr) - (extracted_modules pipeline_tutorial) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/save_restore.v" - (rule (write-file "save_restore_extr.v" - "Require Coq.extraction.Extraction examples.save_restore. -Extraction \"save_restore.ml\" save_restore.prog.")) - (coq.extraction - (prelude save_restore_extr) - (extracted_modules save_restore) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/uart.v" - (rule (write-file "uart_extr.v" - "Require Coq.extraction.Extraction examples.uart. -Extraction \"uart.ml\" uart.prog.")) - (coq.extraction - (prelude uart_extr) - (extracted_modules uart) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/vector.v" - (rule (write-file "vector_extr.v" - "Require Coq.extraction.Extraction examples.vector. -Extraction \"vector.ml\" vector.prog.")) - (coq.extraction - (prelude vector_extr) - (extracted_modules vector) - (theories Ltac2 Koika examples) - (flags "-w" "-overriding-logical-loadpath"))) +(rule + (mode promote) + (alias genrules) + (deps (glob_files *.v) (glob_files *.lv)) + (action (with-stdout-to dune.inc (run ../ruleGen.exe examples %{deps})))) diff --git a/examples/dune.inc b/examples/dune.inc new file mode 100644 index 00000000..e4ff9855 --- /dev/null +++ b/examples/dune.inc @@ -0,0 +1,333 @@ +(subdir collatz.lv.d + (rule + (target collatz.v) + (alias runtest) + (deps (package koika) ../collatz.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir collatz.v.d + (rule + (action + (write-file collatz_extr.v + "Require Coq.extraction.Extraction examples.collatz. +Extraction \"collatz.ml\" collatz.prog.\n"))) + + (coq.extraction + (prelude collatz_extr) + (extracted_modules collatz) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target collatz.v) + (alias runtest) + (deps (package koika) collatz.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir combinational_proof_tutorial.v.d + (rule + (action + (write-file combinational_proof_tutorial_extr.v + "Require Coq.extraction.Extraction examples.combinational_proof_tutorial. +Extraction \"combinational_proof_tutorial.ml\" combinational_proof_tutorial.prog.\n"))) + + (coq.extraction + (prelude combinational_proof_tutorial_extr) + (extracted_modules combinational_proof_tutorial) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target combinational_proof_tutorial.v) + (alias runtest) + (deps (package koika) combinational_proof_tutorial.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir conflicts.v.d + (rule + (action + (write-file conflicts_extr.v + "Require Coq.extraction.Extraction examples.conflicts. +Extraction \"conflicts.ml\" conflicts.prog.\n"))) + + (coq.extraction + (prelude conflicts_extr) + (extracted_modules conflicts) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target conflicts.v) + (alias runtest) + (deps (package koika) conflicts.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir conflicts_modular.v.d + (rule + (action + (write-file conflicts_modular_extr.v + "Require Coq.extraction.Extraction examples.conflicts_modular. +Extraction \"conflicts_modular.ml\" conflicts_modular.prog.\n"))) + + (coq.extraction + (prelude conflicts_modular_extr) + (extracted_modules conflicts_modular) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target conflicts_modular.v) + (alias runtest) + (deps (package koika) conflicts_modular.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir cosimulation.v.d + (rule + (action + (write-file cosimulation_extr.v + "Require Coq.extraction.Extraction examples.cosimulation. +Extraction \"cosimulation.ml\" cosimulation.prog.\n"))) + + (coq.extraction + (prelude cosimulation_extr) + (extracted_modules cosimulation) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target cosimulation.v) + (alias runtest) + (deps (package koika) cosimulation.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir datatypes.v.d + (rule + (action + (write-file datatypes_extr.v + "Require Coq.extraction.Extraction examples.datatypes. +Extraction \"datatypes.ml\" datatypes.prog.\n"))) + + (coq.extraction + (prelude datatypes_extr) + (extracted_modules datatypes) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target datatypes.v) + (alias runtest) + (deps (package koika) datatypes.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir external_rule.v.d + (rule + (action + (write-file external_rule_extr.v + "Require Coq.extraction.Extraction examples.external_rule. +Extraction \"external_rule.ml\" external_rule.prog.\n"))) + + (coq.extraction + (prelude external_rule_extr) + (extracted_modules external_rule) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target external_rule.v) + (alias runtest) + (deps (package koika) external_rule.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir fft.v.d + (rule + (action + (write-file fft_extr.v + "Require Coq.extraction.Extraction examples.fft. +Extraction \"fft.ml\" fft.prog.\n"))) + + (coq.extraction + (prelude fft_extr) + (extracted_modules fft) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target fft.v) + (alias runtest) + (deps (package koika) fft.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir fir.v.d + (rule + (action + (write-file fir_extr.v + "Require Coq.extraction.Extraction examples.fir. +Extraction \"fir.ml\" fir.prog.\n"))) + + (coq.extraction + (prelude fir_extr) + (extracted_modules fir) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target fir.v) + (alias runtest) + (deps (package koika) fir.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir function_call.v.d + (rule + (action + (write-file function_call_extr.v + "Require Coq.extraction.Extraction examples.function_call. +Extraction \"function_call.ml\" function_call.prog.\n"))) + + (coq.extraction + (prelude function_call_extr) + (extracted_modules function_call) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target function_call.v) + (alias runtest) + (deps (package koika) function_call.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir gcd_machine.v.d + (rule + (action + (write-file gcd_machine_extr.v + "Require Coq.extraction.Extraction examples.gcd_machine. +Extraction \"gcd_machine.ml\" gcd_machine.prog.\n"))) + + (coq.extraction + (prelude gcd_machine_extr) + (extracted_modules gcd_machine) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target gcd_machine.v) + (alias runtest) + (deps (package koika) gcd_machine.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir method_call.v.d + (rule + (action + (write-file method_call_extr.v + "Require Coq.extraction.Extraction examples.method_call. +Extraction \"method_call.ml\" method_call.prog.\n"))) + + (coq.extraction + (prelude method_call_extr) + (extracted_modules method_call) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target method_call.o) + (alias runtest) + (deps (package koika) method_call.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir pipeline.v.d + (rule + (action + (write-file pipeline_extr.v + "Require Coq.extraction.Extraction examples.pipeline. +Extraction \"pipeline.ml\" pipeline.prog.\n"))) + + (coq.extraction + (prelude pipeline_extr) + (extracted_modules pipeline) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target pipeline.v) + (alias runtest) + (deps (package koika) pipeline.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir pipeline_tutorial.v.d + (rule + (action + (write-file pipeline_tutorial_extr.v + "Require Coq.extraction.Extraction examples.pipeline_tutorial. +Extraction \"pipeline_tutorial.ml\" pipeline_tutorial.prog.\n"))) + + (coq.extraction + (prelude pipeline_tutorial_extr) + (extracted_modules pipeline_tutorial) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target pipeline_tutorial.v) + (alias runtest) + (deps (package koika) pipeline_tutorial.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir save_restore.v.d + (rule + (action + (write-file save_restore_extr.v + "Require Coq.extraction.Extraction examples.save_restore. +Extraction \"save_restore.ml\" save_restore.prog.\n"))) + + (coq.extraction + (prelude save_restore_extr) + (extracted_modules save_restore) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target save_restore.v) + (alias runtest) + (deps (package koika) save_restore.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir uart.v.d + (rule + (action + (write-file uart_extr.v + "Require Coq.extraction.Extraction examples.uart. +Extraction \"uart.ml\" uart.prog.\n"))) + + (coq.extraction + (prelude uart_extr) + (extracted_modules uart) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target uart.v) + (alias runtest) + (deps (package koika) uart.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir vector.v.d + (rule + (action + (write-file vector_extr.v + "Require Coq.extraction.Extraction examples.vector. +Extraction \"vector.ml\" vector.prog.\n"))) + + (coq.extraction + (prelude vector_extr) + (extracted_modules vector) + (theories Ltac2 Koika examples) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target vector.v) + (alias runtest) + (deps (package koika) vector.ml) + (action (run cuttlec %{deps} -T all -o .)))) + diff --git a/examples/rv/dune b/examples/rv/dune index e85b50c9..bfe12cc9 100644 --- a/examples/rv/dune +++ b/examples/rv/dune @@ -5,30 +5,10 @@ (theories Ltac2 Koika) (flags "-w" "-overriding-logical-loadpath" -nI ../../coq.kernel)) +(include dune.inc) -;; --- DO NOT EDIT BELOW THIS LINE (use ‘make configure’) --- -(dirs :standard _objects) - - -;; -*- dune -*- -(subdir "_objects/rv32e.v" - (rule (write-file "rv32e_extr.v" - "Require Coq.extraction.Extraction rv.rv32e. -Extraction \"rv32e.ml\" rv32e.prog.")) - (coq.extraction - (prelude rv32e_extr) - (extracted_modules rv32e) - (theories Ltac2 Koika rv) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/rv32i.v" - (rule (write-file "rv32i_extr.v" - "Require Coq.extraction.Extraction rv.rv32i. -Extraction \"rv32i.ml\" rv32i.prog.")) - (coq.extraction - (prelude rv32i_extr) - (extracted_modules rv32i) - (theories Ltac2 Koika rv) - (flags "-w" "-overriding-logical-loadpath"))) +(rule + (mode promote) + (alias genrules) + (deps (file rv32i.v) (file rv32e.v)) + (action (with-stdout-to dune.inc (run ../../ruleGen.exe rv %{deps})))) diff --git a/examples/rv/dune.inc b/examples/rv/dune.inc new file mode 100644 index 00000000..57f3d5c0 --- /dev/null +++ b/examples/rv/dune.inc @@ -0,0 +1,38 @@ +(subdir rv32e.v.d + (rule + (action + (write-file rv32e_extr.v + "Require Coq.extraction.Extraction rv.rv32e. +Extraction \"rv32e.ml\" rv32e.prog.\n"))) + + (coq.extraction + (prelude rv32e_extr) + (extracted_modules rv32e) + (theories Ltac2 Koika rv) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target rv32.v) + (alias runtest) + (deps (package koika) rv32e.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir rv32i.v.d + (rule + (action + (write-file rv32i_extr.v + "Require Coq.extraction.Extraction rv.rv32i. +Extraction \"rv32i.ml\" rv32i.prog.\n"))) + + (coq.extraction + (prelude rv32i_extr) + (extracted_modules rv32i) + (theories Ltac2 Koika rv) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target rv32.v) + (alias runtest) + (deps (package koika) rv32i.ml) + (action (run cuttlec %{deps} -T all -o .)))) + diff --git a/flake.nix b/flake.nix index 8e97326c..2e4082c6 100644 --- a/flake.nix +++ b/flake.nix @@ -9,7 +9,7 @@ outputs = { self, flake-utils, nixpkgs, ... }: with flake-utils.lib; let - koikaPkg = { lib, mkCoqDerivation, coq, python3, boost, gtkwave }: mkCoqDerivation rec { + koikaPkg = { lib, mkCoqDerivation, coq, boost, }: mkCoqDerivation rec { pname = "koika"; defaultVersion = "0.0.1"; @@ -47,13 +47,12 @@ mv "$out/lib/koika" "$OCAMLFIND_DESTDIR" ''; - nativeCheckInputs = [ python3 gtkwave ]; # NOTE: Also build the examples, because they use additional parts of # the Dune toolchain. checkPhase = '' runHook preCheck - patchShebangs etc/configure - make VERBOSE=1 tests examples + ./coq.kernel.hack.sh + dune build @runtest runHook postCheck ''; }; diff --git a/ruleGen.ml b/ruleGen.ml new file mode 100644 index 00000000..c15b7af6 --- /dev/null +++ b/ruleGen.ml @@ -0,0 +1,72 @@ +(** Generate build rules for examples and tests *) + +(* Does not currently copy support files from *.etc into output directory. This + is used for further Make-based execution of simulation and synthesis. *) +let generate_rules theory fn = +let base = Filename.remove_extension fn in +let tgt = (match fn with + "method_call.v" -> Printf.sprintf "%s.%s" base "o" + | "rv32i.v" -> Printf.sprintf "rv32.v" + | "rv32e.v" -> Printf.sprintf "rv32.v" + | _ -> Printf.sprintf "%s.%s" base "v") in +match Filename.extension fn with + ".v" -> Printf.printf +{|(subdir %s.d + (rule + (action + (write-file %s_extr.v + "Require Coq.extraction.Extraction %s.%s. +Extraction \"%s.ml\" %s.prog.\n"))) + + (coq.extraction + (prelude %s_extr) + (extracted_modules %s) + (theories Ltac2 Koika %s) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target %s) + (alias runtest) + (deps (package koika) %s.ml) + (action (run cuttlec %%{deps} -T all -o .)))) + +|} + fn base theory base base base base base theory tgt base + + | ".lv" -> (match Filename.extension base with + ".1" -> Printf.printf +{|(subdir %s.d + (rule + (target %s.v) + (alias runtest) + (deps (package koika) ../%s) + (action + (progn + (ignore-stderr (run cuttlec %%{deps} -T all -o . --expect-errors)) + (run touch %%{target}))))) + +|} + fn base fn + + | _ -> Printf.printf +{|(subdir %s.d + (rule + (target %s.v) + (alias runtest) + (deps (package koika) ../%s) + (action + (progn + (run cuttlec %%{deps} -T all -o .) + (run touch %%{target}))))) + +|} + fn base fn) + + | _ -> raise(Failure (Printf.sprintf "cannot generate rules for %s" fn)) + +let () = + let args = Sys.argv |> Array.to_list |> List.tl in + let theory = List.hd args in + let rules = generate_rules theory in + List.tl args |> List.sort String.compare + |> List.iter rules diff --git a/tests/dune b/tests/dune index dfb8ec48..b6f0d7d1 100644 --- a/tests/dune +++ b/tests/dune @@ -7,174 +7,10 @@ (env (dev (flags (:standard -w -39)))) +(include dune.inc) -;; --- DO NOT EDIT BELOW THIS LINE (use ‘make configure’) --- -(dirs :standard _objects) - - -;; -*- dune -*- -(subdir "_objects/cross_cycle.v" - (rule (write-file "cross_cycle_extr.v" - "Require Coq.extraction.Extraction tests.cross_cycle. -Extraction \"cross_cycle.ml\" cross_cycle.prog.")) - (coq.extraction - (prelude cross_cycle_extr) - (extracted_modules cross_cycle) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/double_write.v" - (rule (write-file "double_write_extr.v" - "Require Coq.extraction.Extraction tests.double_write. -Extraction \"double_write.ml\" double_write.prog.")) - (coq.extraction - (prelude double_write_extr) - (extracted_modules double_write) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/errors.v" - (rule (write-file "errors_extr.v" - "Require Coq.extraction.Extraction tests.errors. -Extraction \"errors.ml\" errors.prog.")) - (coq.extraction - (prelude errors_extr) - (extracted_modules errors) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/extcall.v" - (rule (write-file "extcall_extr.v" - "Require Coq.extraction.Extraction tests.extcall. -Extraction \"extcall.ml\" extcall.prog.")) - (coq.extraction - (prelude extcall_extr) - (extracted_modules extcall) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/internal_functions.v" - (rule (write-file "internal_functions_extr.v" - "Require Coq.extraction.Extraction tests.internal_functions. -Extraction \"internal_functions.ml\" internal_functions.prog.")) - (coq.extraction - (prelude internal_functions_extr) - (extracted_modules internal_functions) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/large_writeset.v" - (rule (write-file "large_writeset_extr.v" - "Require Coq.extraction.Extraction tests.large_writeset. -Extraction \"large_writeset.ml\" large_writeset.prog.")) - (coq.extraction - (prelude large_writeset_extr) - (extracted_modules large_writeset) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/muxelim.v" - (rule (write-file "muxelim_extr.v" - "Require Coq.extraction.Extraction tests.muxelim. -Extraction \"muxelim.ml\" muxelim.prog.")) - (coq.extraction - (prelude muxelim_extr) - (extracted_modules muxelim) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/read1_write1_check.v" - (rule (write-file "read1_write1_check_extr.v" - "Require Coq.extraction.Extraction tests.read1_write1_check. -Extraction \"read1_write1_check.ml\" read1_write1_check.prog.")) - (coq.extraction - (prelude read1_write1_check_extr) - (extracted_modules read1_write1_check) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/register_file_bypassing.v" - (rule (write-file "register_file_bypassing_extr.v" - "Require Coq.extraction.Extraction tests.register_file_bypassing. -Extraction \"register_file_bypassing.ml\" register_file_bypassing.prog.")) - (coq.extraction - (prelude register_file_bypassing_extr) - (extracted_modules register_file_bypassing) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/shifts.v" - (rule (write-file "shifts_extr.v" - "Require Coq.extraction.Extraction tests.shifts. -Extraction \"shifts.ml\" shifts.prog.")) - (coq.extraction - (prelude shifts_extr) - (extracted_modules shifts) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/struct_init.v" - (rule (write-file "struct_init_extr.v" - "Require Coq.extraction.Extraction tests.struct_init. -Extraction \"struct_init.ml\" struct_init.prog.")) - (coq.extraction - (prelude struct_init_extr) - (extracted_modules struct_init) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/switches.v" - (rule (write-file "switches_extr.v" - "Require Coq.extraction.Extraction tests.switches. -Extraction \"switches.ml\" switches.prog.")) - (coq.extraction - (prelude switches_extr) - (extracted_modules switches) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/trivial_state_machine.v" - (rule (write-file "trivial_state_machine_extr.v" - "Require Coq.extraction.Extraction tests.trivial_state_machine. -Extraction \"trivial_state_machine.ml\" trivial_state_machine.prog.")) - (coq.extraction - (prelude trivial_state_machine_extr) - (extracted_modules trivial_state_machine) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) - - -;; -*- dune -*- -(subdir "_objects/unpack.v" - (rule (write-file "unpack_extr.v" - "Require Coq.extraction.Extraction tests.unpack. -Extraction \"unpack.ml\" unpack.prog.")) - (coq.extraction - (prelude unpack_extr) - (extracted_modules unpack) - (theories Ltac2 Koika tests) - (flags "-w" "-overriding-logical-loadpath"))) +(rule + (mode promote) + (alias genrules) + (deps (glob_files *.v) (glob_files *.lv)) + (action (with-stdout-to dune.inc (run ../ruleGen.exe tests %{deps})))) diff --git a/tests/dune.inc b/tests/dune.inc new file mode 100644 index 00000000..05485b51 --- /dev/null +++ b/tests/dune.inc @@ -0,0 +1,386 @@ +(subdir arrays.lv.d + (rule + (target arrays.v) + (alias runtest) + (deps (package koika) ../arrays.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir bigint.lv.d + (rule + (target bigint.v) + (alias runtest) + (deps (package koika) ../bigint.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir comparisons.lv.d + (rule + (target comparisons.v) + (alias runtest) + (deps (package koika) ../comparisons.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir cross_cycle.v.d + (rule + (action + (write-file cross_cycle_extr.v + "Require Coq.extraction.Extraction tests.cross_cycle. +Extraction \"cross_cycle.ml\" cross_cycle.prog.\n"))) + + (coq.extraction + (prelude cross_cycle_extr) + (extracted_modules cross_cycle) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target cross_cycle.v) + (alias runtest) + (deps (package koika) cross_cycle.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir datatypes.lv.d + (rule + (target datatypes.v) + (alias runtest) + (deps (package koika) ../datatypes.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir double_write.v.d + (rule + (action + (write-file double_write_extr.v + "Require Coq.extraction.Extraction tests.double_write. +Extraction \"double_write.ml\" double_write.prog.\n"))) + + (coq.extraction + (prelude double_write_extr) + (extracted_modules double_write) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target double_write.v) + (alias runtest) + (deps (package koika) double_write.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir errors.1.lv.d + (rule + (target errors.1.v) + (alias runtest) + (deps (package koika) ../errors.1.lv) + (action + (progn + (ignore-stderr (run cuttlec %{deps} -T all -o . --expect-errors)) + (run touch %{target}))))) + +(subdir errors.v.d + (rule + (action + (write-file errors_extr.v + "Require Coq.extraction.Extraction tests.errors. +Extraction \"errors.ml\" errors.prog.\n"))) + + (coq.extraction + (prelude errors_extr) + (extracted_modules errors) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target errors.v) + (alias runtest) + (deps (package koika) errors.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir extcall.v.d + (rule + (action + (write-file extcall_extr.v + "Require Coq.extraction.Extraction tests.extcall. +Extraction \"extcall.ml\" extcall.prog.\n"))) + + (coq.extraction + (prelude extcall_extr) + (extracted_modules extcall) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target extcall.v) + (alias runtest) + (deps (package koika) extcall.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir internal_functions.v.d + (rule + (action + (write-file internal_functions_extr.v + "Require Coq.extraction.Extraction tests.internal_functions. +Extraction \"internal_functions.ml\" internal_functions.prog.\n"))) + + (coq.extraction + (prelude internal_functions_extr) + (extracted_modules internal_functions) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target internal_functions.v) + (alias runtest) + (deps (package koika) internal_functions.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir large_trace.lv.d + (rule + (target large_trace.v) + (alias runtest) + (deps (package koika) ../large_trace.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir large_writeset.v.d + (rule + (action + (write-file large_writeset_extr.v + "Require Coq.extraction.Extraction tests.large_writeset. +Extraction \"large_writeset.ml\" large_writeset.prog.\n"))) + + (coq.extraction + (prelude large_writeset_extr) + (extracted_modules large_writeset) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target large_writeset.v) + (alias runtest) + (deps (package koika) large_writeset.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir mul.lv.d + (rule + (target mul.v) + (alias runtest) + (deps (package koika) ../mul.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir muxelim.v.d + (rule + (action + (write-file muxelim_extr.v + "Require Coq.extraction.Extraction tests.muxelim. +Extraction \"muxelim.ml\" muxelim.prog.\n"))) + + (coq.extraction + (prelude muxelim_extr) + (extracted_modules muxelim) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target muxelim.v) + (alias runtest) + (deps (package koika) muxelim.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir name_mangling.lv.d + (rule + (target name_mangling.v) + (alias runtest) + (deps (package koika) ../name_mangling.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir read1_write1_check.v.d + (rule + (action + (write-file read1_write1_check_extr.v + "Require Coq.extraction.Extraction tests.read1_write1_check. +Extraction \"read1_write1_check.ml\" read1_write1_check.prog.\n"))) + + (coq.extraction + (prelude read1_write1_check_extr) + (extracted_modules read1_write1_check) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target read1_write1_check.v) + (alias runtest) + (deps (package koika) read1_write1_check.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir register_file_bypassing.v.d + (rule + (action + (write-file register_file_bypassing_extr.v + "Require Coq.extraction.Extraction tests.register_file_bypassing. +Extraction \"register_file_bypassing.ml\" register_file_bypassing.prog.\n"))) + + (coq.extraction + (prelude register_file_bypassing_extr) + (extracted_modules register_file_bypassing) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target register_file_bypassing.v) + (alias runtest) + (deps (package koika) register_file_bypassing.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir shadowing.lv.d + (rule + (target shadowing.v) + (alias runtest) + (deps (package koika) ../shadowing.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir shifts.v.d + (rule + (action + (write-file shifts_extr.v + "Require Coq.extraction.Extraction tests.shifts. +Extraction \"shifts.ml\" shifts.prog.\n"))) + + (coq.extraction + (prelude shifts_extr) + (extracted_modules shifts) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target shifts.v) + (alias runtest) + (deps (package koika) shifts.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir signed.lv.d + (rule + (target signed.v) + (alias runtest) + (deps (package koika) ../signed.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir struct_init.v.d + (rule + (action + (write-file struct_init_extr.v + "Require Coq.extraction.Extraction tests.struct_init. +Extraction \"struct_init.ml\" struct_init.prog.\n"))) + + (coq.extraction + (prelude struct_init_extr) + (extracted_modules struct_init) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target struct_init.v) + (alias runtest) + (deps (package koika) struct_init.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir switches.v.d + (rule + (action + (write-file switches_extr.v + "Require Coq.extraction.Extraction tests.switches. +Extraction \"switches.ml\" switches.prog.\n"))) + + (coq.extraction + (prelude switches_extr) + (extracted_modules switches) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target switches.v) + (alias runtest) + (deps (package koika) switches.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir taint_analysis.lv.d + (rule + (target taint_analysis.v) + (alias runtest) + (deps (package koika) ../taint_analysis.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir tmp_var.lv.d + (rule + (target tmp_var.v) + (alias runtest) + (deps (package koika) ../tmp_var.lv) + (action + (progn + (run cuttlec %{deps} -T all -o .) + (run touch %{target}))))) + +(subdir trivial_state_machine.v.d + (rule + (action + (write-file trivial_state_machine_extr.v + "Require Coq.extraction.Extraction tests.trivial_state_machine. +Extraction \"trivial_state_machine.ml\" trivial_state_machine.prog.\n"))) + + (coq.extraction + (prelude trivial_state_machine_extr) + (extracted_modules trivial_state_machine) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target trivial_state_machine.v) + (alias runtest) + (deps (package koika) trivial_state_machine.ml) + (action (run cuttlec %{deps} -T all -o .)))) + +(subdir unpack.v.d + (rule + (action + (write-file unpack_extr.v + "Require Coq.extraction.Extraction tests.unpack. +Extraction \"unpack.ml\" unpack.prog.\n"))) + + (coq.extraction + (prelude unpack_extr) + (extracted_modules unpack) + (theories Ltac2 Koika tests) + (flags "-w" "-overriding-logical-loadpath")) + + (rule + (target unpack.v) + (alias runtest) + (deps (package koika) unpack.ml) + (action (run cuttlec %{deps} -T all -o .)))) +