diff --git a/share/pulse/examples/NuPool.fst b/lib/pulse/lib/Pulse.Lib.Task.fst
similarity index 99%
rename from share/pulse/examples/NuPool.fst
rename to lib/pulse/lib/Pulse.Lib.Task.fst
index 78ab3be11..ea2c3bfb2 100644
--- a/share/pulse/examples/NuPool.fst
+++ b/lib/pulse/lib/Pulse.Lib.Task.fst
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 
-module NuPool
+module Pulse.Lib.Task
 #lang-pulse
 
 open Pulse.Lib.Pervasives
diff --git a/lib/pulse/lib/Pulse.Lib.Task.fsti b/lib/pulse/lib/Pulse.Lib.Task.fsti
index e28eb7092..b6fd106df 100644
--- a/lib/pulse/lib/Pulse.Lib.Task.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Task.fsti
@@ -1,5 +1,5 @@
 (*
-   Copyright 2023 Microsoft Research
+   Copyright 2024 Microsoft Research
 
    Licensed under the Apache License, Version 2.0 (the "License");
    you may not use this file except in compliance with the License.
@@ -15,105 +15,85 @@
 *)
 
 module Pulse.Lib.Task
+#lang-pulse
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Pledge
-module T = FStar.Tactics
+module T = FStar.Tactics.V2
 
+val handle : Type0
 val pool : Type0
-val pool_alive : (#[T.exact (`1.0R)]p : perm) -> pool -> slprop
-val pool_done : pool -> slprop
-
-val setup_pool (n:pos)
-  : stt pool emp (fun p -> pool_alive #1.0R p)
-
-val task_handle : pool -> a:Type0 -> (a -> slprop) -> Type0
-val joinable : #p:pool -> #a:Type0 -> #post:_ -> th:(task_handle p a post) -> slprop
-val joined   : #p:pool -> #a:Type0 -> #post:_ -> th:(task_handle p a post) -> slprop
-
-val handle_solved
-  (#p : pool) 
-  (#a : Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : slprop
-
-(* NOTE! Spawn only requires an *epsilon* of permission over the pool.
-We do not have to be exclusive owners of it in order to queue a job,
-even if that modifies it. How to model this under the hood? *)
-val spawn
-  (#a : Type0)
-  (#pre : slprop) (#post : a -> slprop)
-  (p : pool)
-  (#[T.exact (`1.0R)] e : perm)
-  ($f : unit -> stt a pre (fun (x:a) -> post x))
-  : stt (task_handle p a post)
-        (pool_alive #e p ** pre)
-        (fun th -> pool_alive #e p ** joinable th)
-
-(* Spawn of a unit-returning task with no intention to join, simpler. *)
-val spawn_
-  (#pre #post : _)
-  (p:pool)
-  (#[T.exact (`1.0R)] e : perm)
+val pool_alive (#[T.exact (`1.0R)] f : perm) (p:pool) : slprop
+
+val joinable (p: pool) (post: slprop) (h: handle) : slprop
+
+fn spawn
+  (p: pool)
+  (#pf: perm)
+  (#pre: slprop)
+  (#post: slprop)
   (f : unit -> stt unit pre (fun _ -> post))
-  : stt unit (pool_alive #e p ** pre)
-             (fun prom -> pool_alive #e p ** pledge emp_inames (pool_done p) post)
+  requires pool_alive #pf p ** pre
+  returns h : handle
+  ensures pool_alive #pf p ** joinable p post h
 
-(* If the pool is done, all pending joinable threads must be done *)
-val must_be_done
+val pool_done (p:pool) : slprop
+
+ghost
+fn disown
   (#p : pool)
-  (#a: Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt_ghost unit emp_inames (pool_done p ** joinable th) (fun () -> pool_done p ** handle_solved th)
-
-val join0
-  (#p:pool)
-  (#a:Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt unit (joinable th) (fun () -> handle_solved th)
-
-val extract
-  (#p:pool)
-  (#a:Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt a (handle_solved th) (fun x -> post x)
-  
-val share_alive
+  (#post : slprop)
+  (h : handle)
+  requires joinable p post h
+  ensures  pledge [] (pool_done p) post
+
+(* spawn + disown *)
+fn spawn_
+  (p: pool)
+  (#pf : perm)
+  (#pre : slprop)
+  (#post : slprop)
+  (f : unit -> stt unit (pre) (fun _ -> post))
+  requires pool_alive #pf p ** pre
+  ensures pool_alive #pf p ** pledge [] (pool_done p) post
+
+fn await
+  (#p: pool)
+  (#post : slprop)
+  (h : handle)
+  (#f : perm)
+  requires pool_alive #f p ** joinable p post h
+  ensures pool_alive #f p ** post
+
+fn await_pool
   (p:pool)
-  (e:perm)
-  : stt_ghost unit
-              emp_inames
-              (pool_alive #e p)
-              (fun () -> pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p)
+  (#is:inames)
+  (#f:perm)
+  (q : slprop)
+  requires pool_alive #f p ** pledge is (pool_done p) q
+  ensures pool_alive #f p ** q
 
-val gather_alive
+fn teardown_pool
   (p:pool)
-  (e:perm)
-  : stt_ghost unit
-              emp_inames
-              (pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p)
-              (fun () -> pool_alive #e p)
-
-val join
-  (#p:pool)
-  (#a:Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt a (joinable th) (fun x -> post x)
-
-(* We must exclusively own the pool in order to terminate it. *)
-val teardown_pool
+  requires pool_alive p
+  ensures pool_done p
+
+ghost
+fn share_alive
   (p:pool)
-  : stt unit (pool_alive #1.0R p) (fun _ -> pool_done p)
+  (e:perm)
+  requires pool_alive #e p
+  ensures pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p
 
-(* Or, have at least an epsilon of permission over it, and know that
-the rest of it (1-e) is "sunk" into the pool itself. *)
-val teardown_pool'
-  (#is:inames)
-  (p:pool) (f:perm{f <. 1.0R})
-  : stt unit (pool_alive #f p ** pledge is (pool_done p) (pool_alive #(1.0R -. f) p))
-             (fun _ -> pool_done p)
+ghost
+fn gather_alive
+  (p:pool)
+  (e:perm)
+  requires pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p
+  ensures pool_alive #e p
+
+fn setup_pool
+  (n: pos)
+  requires emp
+  returns p : pool
+  ensures pool_alive p
diff --git a/qs/Makefile b/qs/Makefile
index f91ac2e48..985608ad9 100644
--- a/qs/Makefile
+++ b/qs/Makefile
@@ -5,15 +5,19 @@ OTHERFLAGS += --ext pulse:extract_ocaml_bare
 DEPFLAGS += --extract '-*'
 DEPFLAGS += --extract +Quicksort
 DEPFLAGS += --extract +Pulse.Lib.Dv
-# DEPFLAGS += --extract +NuPool
+# DEPFLAGS += --extract +Pulse.Lib.Task
 # DEPFLAGS += --extract +Pulse.Class.Duplicable
 # DEPFLAGS += --extract +FStar.Dyn # wrong. it's int FStarC_Dyn.ml
 
 include fstar.mk
-all: _output/Quicksort_Task.exe
 
-_output/Quicksort_Task.exe: $(ALL_ML_FILES)
-	eval $$(OPAMSWITCH=5.1.1 opam env) && /home/guido/.opam/5.1.1/bin/dune build --root=dune
+.PHONY: all
+all: run
 
-run:
+.PHONY: dune
+dune: $(ALL_ML_FILES)
+	opam exec --switch=5.1.1 -- dune build --root=dune
+
+.PHONY: run
+run: dune
 	./dune/_build/default/driver.exe
diff --git a/qs/README.md b/qs/README.md
new file mode 100644
index 000000000..9edde3b76
--- /dev/null
+++ b/qs/README.md
@@ -0,0 +1,9 @@
+# Parallel quicksort extracted to OCaml 5
+
+This directory contains the build infrastructure to extract the Quicksort.Task file to OCaml, and build it with OCaml 5.1.1 and domainslib.
+
+```shell
+opam switch create 5.1.1
+opam install --switch=5.1.1 domainslib
+make
+```
diff --git a/qs/dune/NuPool.ml b/qs/dune/NuPool.ml
deleted file mode 120000
index ff2c8dfa5..000000000
--- a/qs/dune/NuPool.ml
+++ /dev/null
@@ -1 +0,0 @@
-../NuPool.ml
\ No newline at end of file
diff --git a/qs/NuPool.ml b/qs/dune/Pulse_Lib_Task.ml
similarity index 100%
rename from qs/NuPool.ml
rename to qs/dune/Pulse_Lib_Task.ml
diff --git a/qs/fstar.mk b/qs/fstar.mk
index 4f3d6c560..d0d99fd64 100644
--- a/qs/fstar.mk
+++ b/qs/fstar.mk
@@ -20,7 +20,7 @@ include common.mk
 .DEFAULT_GOAL := all
 
 # Set a default FSTAR_EXE for most clients.
-FSTAR_EXE ?= $(FSTAR_ROOT)/bin/fstar.exe
+FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 FSTAR_EXE := $(abspath $(FSTAR_EXE))
 export FSTAR_EXE
 
diff --git a/share/pulse/examples/MSort.Task.fst b/share/pulse/examples/MSort.Task.fst
index d6dc3c9b5..00ebd0f13 100644
--- a/share/pulse/examples/MSort.Task.fst
+++ b/share/pulse/examples/MSort.Task.fst
@@ -22,7 +22,7 @@ module S = FStar.Seq
 module SZ = FStar.SizeT
 open MSort.SeqLemmas
 open MSort.Base
-open NuPool
+open Pulse.Lib.Task
 
 
 fn rec t_msort_par
diff --git a/share/pulse/examples/NuPool.fsti b/share/pulse/examples/NuPool.fsti
deleted file mode 100644
index 5aa1988e0..000000000
--- a/share/pulse/examples/NuPool.fsti
+++ /dev/null
@@ -1,99 +0,0 @@
-(*
-   Copyright 2024 Microsoft Research
-
-   Licensed under the Apache License, Version 2.0 (the "License");
-   you may not use this file except in compliance with the License.
-   You may obtain a copy of the License at
-
-       http://www.apache.org/licenses/LICENSE-2.0
-
-   Unless required by applicable law or agreed to in writing, software
-   distributed under the License is distributed on an "AS IS" BASIS,
-   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-   See the License for the specific language governing permissions and
-   limitations under the License.
-*)
-
-module NuPool
-#lang-pulse
-
-open Pulse.Lib.Pervasives
-open Pulse.Lib.Pledge
-module T = FStar.Tactics.V2
-
-val handle : Type0
-val pool : Type0
-val pool_alive (#[T.exact (`1.0R)] f : perm) (p:pool) : slprop
-
-val joinable (p: pool) (post: slprop) (h: handle) : slprop
-
-fn spawn
-  (p: pool)
-  (#pf: perm)
-  (#pre: slprop)
-  (#post: slprop)
-  (f : unit -> stt unit pre (fun _ -> post))
-  requires pool_alive #pf p ** pre
-  returns h : handle
-  ensures pool_alive #pf p ** joinable p post h
-
-val pool_done (p:pool) : slprop
-
-ghost
-fn disown
-  (#p : pool)
-  (#post : slprop)
-  (h : handle)
-  requires joinable p post h
-  ensures  pledge [] (pool_done p) post
-
-(* spawn + disown *)
-fn spawn_
-  (p: pool)
-  (#pf : perm)
-  (#pre : slprop)
-  (#post : slprop)
-  (f : unit -> stt unit (pre) (fun _ -> post))
-  requires pool_alive #pf p ** pre
-  ensures pool_alive #pf p ** pledge [] (pool_done p) post
-
-fn await
-  (#p: pool)
-  (#post : slprop)
-  (h : handle)
-  (#f : perm)
-  requires pool_alive #f p ** joinable p post h
-  ensures pool_alive #f p ** post
-
-fn await_pool
-  (p:pool)
-  (#is:inames)
-  (#f:perm)
-  (q : slprop)
-  requires pool_alive #f p ** pledge is (pool_done p) q
-  ensures pool_alive #f p ** q
-
-fn teardown_pool
-  (p:pool)
-  requires pool_alive p
-  ensures pool_done p
-
-ghost
-fn share_alive
-  (p:pool)
-  (e:perm)
-  requires pool_alive #e p
-  ensures pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p
-
-ghost
-fn gather_alive
-  (p:pool)
-  (e:perm)
-  requires pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p
-  ensures pool_alive #e p
-
-fn setup_pool
-  (n: pos)
-  requires emp
-  returns p : pool
-  ensures pool_alive p
diff --git a/share/pulse/examples/Quicksort.Task.fst b/share/pulse/examples/Quicksort.Task.fst
index 9f956046c..447de2faa 100644
--- a/share/pulse/examples/Quicksort.Task.fst
+++ b/share/pulse/examples/Quicksort.Task.fst
@@ -23,7 +23,7 @@ module R = Pulse.Lib.Reference
 module SZ = FStar.SizeT
 module GSet = FStar.GhostSet
 
-module T = NuPool
+module T = Pulse.Lib.Task
 open Quicksort.Base
 open Pulse.Lib.Pledge
 
diff --git a/share/pulse/examples/parix/ParallelFor.fst b/share/pulse/examples/parix/ParallelFor.fst
index 11a22f99b..51554f769 100644
--- a/share/pulse/examples/parix/ParallelFor.fst
+++ b/share/pulse/examples/parix/ParallelFor.fst
@@ -19,7 +19,7 @@ module ParallelFor
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Fixpoints
-open NuPool
+open Pulse.Lib.Task
 open FStar.Real
 open Pulse.Lib.Pledge
 open Pulse.Lib.OnRange
diff --git a/share/pulse/examples/parix/TaskPool.Examples.fst b/share/pulse/examples/parix/TaskPool.Examples.fst
index 5e3cb6fee..52500effa 100644
--- a/share/pulse/examples/parix/TaskPool.Examples.fst
+++ b/share/pulse/examples/parix/TaskPool.Examples.fst
@@ -19,7 +19,7 @@ module TaskPool.Examples
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Pledge
-open NuPool
+open Pulse.Lib.Task
 
 assume
 val qsv : nat -> slprop