From 3e196cd7a54487b6b6670a9a42b0408eda71c416 Mon Sep 17 00:00:00 2001
From: Max Nowak <max.nowak.j@gmail.com>
Date: Thu, 9 Jan 2025 14:39:15 -0800
Subject: [PATCH] more docs

---
 LeanBoogie/Dsl.lean          | 7 +++++++
 LeanBoogie/Spec/ITree0W.lean | 6 +++++-
 lake-manifest.json           | 6 +++---
 lakefile.lean                | 7 +------
 4 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/LeanBoogie/Dsl.lean b/LeanBoogie/Dsl.lean
index 7486ed8..9fdfa80 100644
--- a/LeanBoogie/Dsl.lean
+++ b/LeanBoogie/Dsl.lean
@@ -163,6 +163,13 @@ variable {E : Q(Type -> Type)}
      and it decides to true. If no blocks match, we `spin`.
      We currently use this approach.
      This approach does not faithfully model Boogie semantics, and we should move away from it.
+
+  ### Obtaining executable code
+  When you do use `AssumeAssert` and `Choice` (See (2) in the previous section), you may want to obtain
+  executable code. For `AssumeAssert` this is easy: You simply provide a proof via an axiom, e.g. `sorry`.
+  For `Choice` this is not as straightforward. However, often programs are only non-deterministic on
+  the surface, and the leading assumes for each block are disjoint, in which case we would still
+  like to avoid forking the entire program state.
 -/
 
 
diff --git a/LeanBoogie/Spec/ITree0W.lean b/LeanBoogie/Spec/ITree0W.lean
index 41b63e6..cdc89a5 100644
--- a/LeanBoogie/Spec/ITree0W.lean
+++ b/LeanBoogie/Spec/ITree0W.lean
@@ -4,7 +4,11 @@ import LeanBoogie.Spec.Theta
 namespace LeanBoogie
 open ITree
 
--- # ITree Specs Without Effects [DM4Ever]
+/- # ITree Specs Without Effects [DM4Ever]
+  Without effects, if our tree diverges, we know that `spin` is the canonical representative of it,
+  and for convergence it must be `.ret _`.
+  With effects, this gets non-trivial, and we might have
+-/
 -- See section 4 of "Dijkstra Monads for ever".
 
 -- Corresponding computation monad: `ITree Empty`.
diff --git a/lake-manifest.json b/lake-manifest.json
index 3f01a0a..cafa7d2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -81,14 +81,14 @@
    "inputRev": "v4.12.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/Kiiyya/QpfTypes.git",
+  {"url": "https://github.com/alexkeizer/QpfTypes.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "67e99ac5339969f1fe220100c3c5f05ea37e20f9",
+   "rev": "9cfc50cfa0dc561f5b7a1bf08e693b2a52172383",
    "name": "qpf",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "67e99ac5339969f1fe220100c3c5f05ea37e20f9",
+   "inputRev": "9cfc50cfa0dc561f5b7a1bf08e693b2a52172383",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
diff --git a/lakefile.lean b/lakefile.lean
index 5740f24..6c6a4fd 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,11 +6,6 @@ package "lean-boogie" where
 
 @[default_target]
 lean_lib LeanBoogie where
-  -- ## for 4.12:
-  require qpf from git "https://github.com/Kiiyya/QpfTypes.git" @ "67e99ac5339969f1fe220100c3c5f05ea37e20f9" -- https://github.com/alexkeizer/QpfTypes/pull/52
+  require qpf from git "https://github.com/alexkeizer/QpfTypes.git" @ "9cfc50cfa0dc561f5b7a1bf08e693b2a52172383"
   require auto from git "https://github.com/leanprover-community/lean-auto.git" @ "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a" -- 4.12
   require Duper from git "https://github.com/leanprover-community/duper.git" @ "25c3ea88da2505158998eea07f40b07c0cdfe5ba"
-
--- @[default_target]
--- lean_exe "lean-boogie" where
---   root := `Main