Skip to content

Commit

Permalink
Update QS
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Dec 27, 2024
1 parent 0b63b0f commit aa7f0d1
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 1 deletion.
13 changes: 12 additions & 1 deletion qs/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -24,3 +34,4 @@ test: run
.PHONY: run
run: dune
./dune/_build/default/driver.exe
endif
3 changes: 3 additions & 0 deletions qs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
8 changes: 8 additions & 0 deletions qs/dune/Pulse_Lib_Dv.ml
Original file line number Diff line number Diff line change
@@ -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 ()

0 comments on commit aa7f0d1

Please sign in to comment.