- upgrade to opam 2 package

- make opam package include files required for building rmem

4 files changed, 10 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index 14c7b5d..8167ec9 100644
--- a/Makefile
+++ b/Makefile
@@ -344,6 +344,8 @@ generated_definitions/coq/$(ARCH)/riscv_duopod.vo: generated_definitions/coq/$(A
 echo_rmem_srcs:
 	echo $(SAIL_RMEM_SRCS)
 
+RMEM_FILES = generated_definitions/for-rmem/riscv.lem generated_definitions/for-rmem/riscv_types.lem generated_definitions/for-rmem/riscv_toFromInterp2.ml generated_definitions/for-rmem/riscv.defs
+
 riscv_rmem: generated_definitions/for-rmem/riscv.lem
 riscv_rmem: generated_definitions/for-rmem/riscv_toFromInterp2.ml
 riscv_rmem: generated_definitions/for-rmem/riscv.defs
@@ -369,7 +371,7 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS)
 
 FORCE:
 
-SHARE_FILES:=$(wildcard model/*.sail) $(wildcard c_emulator/*.c) $(wildcard c_emulator/*.h)
+SHARE_FILES:=$(wildcard model/*.sail) $(wildcard c_emulator/*.c) $(wildcard c_emulator/*.h) $(wildcard handwritten_support/*.lem) $(wildcard handwritten_support/hgen/*.hgen) $(wildcard handwritten_support/0.11/*.lem) $(RMEM_FILES)
 sail-riscv.install: FORCE
 	echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install
 	echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install
@@ -377,6 +379,7 @@ sail-riscv.install: FORCE
 opam-build:
 	$(MAKE) ARCH=64 c_emulator/riscv_sim_RV64
 	$(MAKE) ARCH=32 c_emulator/riscv_sim_RV32
+	$(MAKE) riscv_rmem
 
 opam-install:
 	if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi
diff --git a/descr b/descr
deleted file mode 100644
index e44ab06..0000000
--- a/descr
+++ /dev/null
@@ -1 +0,0 @@
-This package installs a RISC-V emulator (32 and 64 bits) built form the Sail model at https://github.com/rems-project/sail-riscv
diff --git a/opam b/opam
index 9622fea..43f5b57 100644
--- a/opam
+++ b/opam
@@ -1,4 +1,4 @@
-opam-version: "1.2"
+opam-version: "2.0"
 name: "sail-riscv"
 version: "0.4"
 maintainer: "Sail Devs <cl-sail-dev@lists.cam.ac.uk>"
@@ -16,9 +16,10 @@ authors: [
 homepage: "https://github.com/rems-project/sail-riscv/"
 bug-reports: "https://github.com/rems-project/sail-riscv/issues"
 license: "BSD3"
-dev-repo: "https://github.com/rems-project/sail-riscv.git"
+dev-repo: "git+https://github.com/rems-project/sail-riscv.git"
 build: [make "LEM_DIR=%{lem:share}%" "SAIL_DIR=%{sail:share}%" "SAIL=sail" "opam-build"]
 depends: [
+  "ocaml" {>= "4.06.1"}
   "ocamlfind"
   "ocamlbuild"
   "lem"
@@ -27,4 +28,5 @@ depends: [
   "conf-gmp"
   "conf-zlib"
 ]
-available: [ocaml-version >= "4.06.1"]
+synopsis:
+  "This package installs a RISC-V emulator (32 and 64 bits) built form the Sail model at https://github.com/rems-project/sail-riscv"
diff --git a/sail-riscv.install b/sail-riscv.install
index ce50f55..5702ea6 100644
--- a/sail-riscv.install
+++ b/sail-riscv.install
@@ -1,2 +1,2 @@
 bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]
-share: [ "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/prelude_mapping.sail" {"model/prelude_mapping.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/riscv_duopod.sail" {"model/riscv_duopod.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/main.sail" {"model/main.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} ]
+share: [ "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/prelude_mapping.sail" {"model/prelude_mapping.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_iris.sail" {"model/riscv_iris.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "model/riscv_duopod.sail" {"model/riscv_duopod.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/main.sail" {"model/main.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_termination_duo.sail" {"model/riscv_termination_duo.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]