diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2022-11-16 17:40:17 +0000 |
|---|---|---|
| committer | Philipp Tomsich <philipp.tomsich@vrull.eu> | 2023-05-31 00:27:23 -0700 |
| commit | 6693700ad7509c4fff3bb22416048dbe0ea0a0d8 (patch) | |
| tree | 5a027faec7873ec925edf77171514aefed994160 | |
| parent | 566c58eb5a8aa26c2feb8529f2402b5b796ac552 (diff) | |
| download | sail-riscv-6693700ad7509c4fff3bb22416048dbe0ea0a0d8.zip sail-riscv-6693700ad7509c4fff3bb22416048dbe0ea0a0d8.tar.gz sail-riscv-6693700ad7509c4fff3bb22416048dbe0ea0a0d8.tar.bz2 | |
Add opam packaging for the Coq output
| -rw-r--r-- | Makefile | 11 | ||||
| -rw-r--r-- | coq-sail-riscv.opam | 35 |
2 files changed, 46 insertions, 0 deletions
@@ -385,6 +385,17 @@ endif generated_definitions/coq/$(ARCH)/riscv.vo: generated_definitions/coq/$(ARCH)/riscv_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo +riscv_coq_install: + if [ ! -f generated_definitions/coq/RV64/riscv.v ]; then echo RV64 has not been built; false; fi + if [ ! -f generated_definitions/coq/RV32/riscv.v ]; then echo RV32 has not been built; false; fi + install -d `coqc -where`/user-contrib/Riscv_common + install -d `coqc -where`/user-contrib/RV64 + install -d `coqc -where`/user-contrib/RV32 + install handwritten_support/*.v* `coqc -where`/user-contrib/Riscv_common + install generated_definitions/coq/RV64/* `coqc -where`/user-contrib/RV64 + install generated_definitions/coq/RV32/* `coqc -where`/user-contrib/RV32 +.PHONY: riscv_coq_install + echo_rmem_srcs: echo $(SAIL_RMEM_SRCS) diff --git a/coq-sail-riscv.opam b/coq-sail-riscv.opam new file mode 100644 index 0000000..a9879f2 --- /dev/null +++ b/coq-sail-riscv.opam @@ -0,0 +1,35 @@ +opam-version: "2.0" +name: "coq-sail-riscv" +version: "0.5" +maintainer: "Sail Devs <cl-sail-dev@lists.cam.ac.uk>" +authors: [ + "Alasdair Armstrong" + "Thomas Bauereiss" + "Brian Campbell" + "Shaked Flur" + "Jonathan French" + "Prashanth Mundkur" + "Robert Norton" + "Christopher Pulte" + "Peter Sewell" +] +homepage: "https://github.com/rems-project/sail-riscv/" +bug-reports: "https://github.com/rems-project/sail-riscv/issues" +license: "BSD3" +dev-repo: "git+https://github.com/rems-project/sail-riscv.git" +build: [ + [make "ARCH=RV64" "riscv_coq_build"] + [make "ARCH=RV32" "riscv_coq_build"] +] +install: [make "riscv_coq_install"] +depends: [ + "ocaml" {>= "4.06.1"} + "ocamlfind" + "ocamlbuild" + "sail" + "coq-sail" + "conf-gmp" + "conf-zlib" +] +synopsis: + "A model of the RISC-V instruction set architecture in Coq, generated from Sail" |