Skip to content

Commit

Permalink
Remove ability to compile to OCaml
Browse files Browse the repository at this point in the history
This will allow the OCaml backend to be improved in the Sail compiler.
  • Loading branch information
Timmmm committed Sep 16, 2024
1 parent 3fb5280 commit 6e0b5c4
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 13 deletions.
4 changes: 0 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -228,10 +228,6 @@ riscv.smt_model: $(SAIL_SRCS)
cgen: $(SAIL_SRCS) model/main.sail
$(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail

generated_definitions/ocaml/$(ARCH)/riscv.ml: $(SAIL_SRCS) Makefile
mkdir -p generated_definitions/ocaml/$(ARCH)
$(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_definitions/ocaml/$(ARCH) -o riscv $(SAIL_SRCS)

cloc:
cloc --by-file --force-lang C,sail $(SAIL_SRCS)

Expand Down
9 changes: 0 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -204,15 +204,6 @@ Those tests have also been run on RISC-V hardware, on a SiFive RISC-V
FU540 multicore proto board (Freedom Unleashed), kindly on loan from
Imperas. To date, only sequentially consistent behaviour was observed there.

Use in test generation
----------------------

The Sail OCaml backend can produce QuickCheck-style random generators for
types in Sail specifications, which have been used to produce random
instructions sequences for testing. The generation of individual
types can be overridden by the developer to, for example, remove
implementation-specific instructions or introduce register biasing.

Generating theorem-prover definitions
--------------------------------------

Expand Down

0 comments on commit 6e0b5c4

Please sign in to comment.