File tree 2 files changed +46
-0
lines changed
2 files changed +46
-0
lines changed Original file line number Diff line number Diff line change @@ -385,6 +385,17 @@ endif
385
385
386
386
generated_definitions/coq/$(ARCH ) /riscv.vo : generated_definitions/coq/$(ARCH ) /riscv_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo
387
387
388
+ riscv_coq_install :
389
+ if [ ! -f generated_definitions/coq/RV64/riscv.v ]; then echo RV64 has not been built; false ; fi
390
+ if [ ! -f generated_definitions/coq/RV32/riscv.v ]; then echo RV32 has not been built; false ; fi
391
+ install -d ` coqc -where` /user-contrib/Riscv_common
392
+ install -d ` coqc -where` /user-contrib/RV64
393
+ install -d ` coqc -where` /user-contrib/RV32
394
+ install handwritten_support/* .v* ` coqc -where` /user-contrib/Riscv_common
395
+ install generated_definitions/coq/RV64/* ` coqc -where` /user-contrib/RV64
396
+ install generated_definitions/coq/RV32/* ` coqc -where` /user-contrib/RV32
397
+ .PHONY : riscv_coq_install
398
+
388
399
echo_rmem_srcs :
389
400
echo $(SAIL_RMEM_SRCS )
390
401
Original file line number Diff line number Diff line change
1
+ opam-version: "2.0"
2
+ name: "coq-sail-riscv"
3
+ version: "0.5"
4
+ maintainer: "Sail Devs <cl-sail-dev@lists.cam.ac.uk>"
5
+ authors: [
6
+ "Alasdair Armstrong"
7
+ "Thomas Bauereiss"
8
+ "Brian Campbell"
9
+ "Shaked Flur"
10
+ "Jonathan French"
11
+ "Prashanth Mundkur"
12
+ "Robert Norton"
13
+ "Christopher Pulte"
14
+ "Peter Sewell"
15
+ ]
16
+ homepage: "https://github.com/rems-project/sail-riscv/"
17
+ bug-reports: "https://github.com/rems-project/sail-riscv/issues"
18
+ license: "BSD3"
19
+ dev-repo: "git+https://github.com/rems-project/sail-riscv.git"
20
+ build: [
21
+ [make "ARCH=RV64" "riscv_coq_build"]
22
+ [make "ARCH=RV32" "riscv_coq_build"]
23
+ ]
24
+ install: [make "riscv_coq_install"]
25
+ depends: [
26
+ "ocaml" {>= "4.06.1"}
27
+ "ocamlfind"
28
+ "ocamlbuild"
29
+ "sail"
30
+ "coq-sail"
31
+ "conf-gmp"
32
+ "conf-zlib"
33
+ ]
34
+ synopsis:
35
+ "A model of the RISC-V instruction set architecture in Coq, generated from Sail"
You can’t perform that action at this time.
0 commit comments