diff --git a/qs/Makefile b/qs/Makefile index 94a878849..30b9e65aa 100644 --- a/qs/Makefile +++ b/qs/Makefile @@ -4,13 +4,23 @@ OTHERFLAGS += --ext pulse:extract_ocaml_bare DEPFLAGS += --extract '-*' DEPFLAGS += --extract +Quicksort -DEPFLAGS += --extract +Pulse.Lib.Dv +# DEPFLAGS += --extract +Pulse.Lib.Dv # DEPFLAGS += --extract +Pulse.Lib.Task # DEPFLAGS += --extract +Pulse.Class.Duplicable # DEPFLAGS += --extract +FStar.Dyn # wrong. it's int FStarC_Dyn.ml include fstar.mk +# This makefile only does something if a 5.1.1 OPAM switch is available. +HAVE_511 != opam env --switch=5.1.1 2>/dev/null # only outputs to stdout on success + +ifeq ($(HAVE_511),) +_ != echo "OPAM switch 5.1.1 does not seem installed, not doing anything" > /dev/tty +.PHONY: all test +all: +test: +else + .PHONY: all all: dune @@ -24,3 +34,4 @@ test: run .PHONY: run run: dune ./dune/_build/default/driver.exe +endif diff --git a/qs/README.md b/qs/README.md index 9edde3b76..c99c4d34f 100644 --- a/qs/README.md +++ b/qs/README.md @@ -7,3 +7,6 @@ opam switch create 5.1.1 opam install --switch=5.1.1 domainslib make ``` + +Note: the Makefile here will not do anything if a 5.1.1 switch +is not installed. Our CI does not test this directory. diff --git a/qs/dune/Pulse_Lib_Dv.ml b/qs/dune/Pulse_Lib_Dv.ml new file mode 100644 index 000000000..add7343ec --- /dev/null +++ b/qs/dune/Pulse_Lib_Dv.ml @@ -0,0 +1,8 @@ +(* This is a slightly edited version of lib/pulse/lib/ml/Pulse_Lib_Dv.ml, to make it work in OCaml 5 (just remove the val) *) + +let while_ cond body = + while (cond ()) do + body () + done + +let rec unreachable () : 'a = unreachable ()