Update to isabelle 2022

flake.nix

@@ -8,7 +8,7 @@
 
     nixpkgs.follows = "haskellNix/nixpkgs-unstable";
 
-    isabelle-nixpkgs.url = "nixpkgs/nixos-22.05";
+    isabelle-nixpkgs.url = "nixpkgs/nixpkgs-unstable";
 
     nixLsp.url = "github:oxalica/nil";
 
@@ -66,6 +66,7 @@
               (with scripts; [
                 build-marlowe-proofs
                 edit-marlowe-proofs
+                vscode-marlowe-proofs
                 build-marlowe-docs
               ]
               ) ++

isabelle/CodeExports/CodeExports.thy

@@ -39,7 +39,7 @@ code_printing
   \<comment> \<open>into Haskell string. Because this is a textual rewrite, we need to force the\<close>
   \<comment> \<open>generation of String.implode\<close>
   | constant "BS :: string \<Rightarrow> ByteString"
-      \<rightharpoonup> (Haskell) "Stringa.implode"
+      \<rightharpoonup> (Haskell) "Str.implode"
 
 
 text \<open>With a \<^bold>\<open>code\_identifier\<close> we hint what the name of the module should be.\<close>

isabelle/generated/Examples/Swap.hs

@@ -14,7 +14,7 @@ import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
   String, Bool(True, False), Maybe(Nothing, Just));
 import qualified Prelude;
 import qualified Semantics;
-import qualified Stringa;
+import qualified Str;
 import qualified SemanticsTypes;
 import qualified Arith;
 
@@ -59,62 +59,62 @@ swap p1 p2 =
       (makePayment p1 p2 (makePayment p2 p1 SemanticsTypes.Close)));
 
 adaToken :: SemanticsTypes.Token;
-adaToken = SemanticsTypes.Token (Stringa.implode []) (Stringa.implode []);
+adaToken = SemanticsTypes.Token (Str.implode []) (Str.implode []);
 
 adaProvider :: SemanticsTypes.Party;
 adaProvider =
   SemanticsTypes.Role
-    (Stringa.implode
-      [Stringa.Char True False False False False False True False,
-        Stringa.Char False False True False False True True False,
-        Stringa.Char True False False False False True True False,
-        Stringa.Char False False False False False True False False,
-        Stringa.Char False False False False True False True False,
-        Stringa.Char False True False False True True True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False True True False True True True False,
-        Stringa.Char True False False True False True True False,
-        Stringa.Char False False True False False True True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char True False False False False False True False,
+        Str.Char False False True False False True True False,
+        Str.Char True False False False False True True False,
+        Str.Char False False False False False True False False,
+        Str.Char False False False False True False True False,
+        Str.Char False True False False True True True False,
+        Str.Char True True True True False True True False,
+        Str.Char False True True False True True True False,
+        Str.Char True False False True False True True False,
+        Str.Char False False True False False True True False,
+        Str.Char True False True False False True True False,
+        Str.Char False True False False True True True False]);
 
 dollarToken :: SemanticsTypes.Token;
 dollarToken =
   SemanticsTypes.Token
-    (Stringa.implode
-      [Stringa.Char False False False True True True False False,
-        Stringa.Char True False True False True True False False,
-        Stringa.Char False True False False False True True False,
-        Stringa.Char False True False False False True True False,
-        Stringa.Char False True True False True True False False,
-        Stringa.Char True False True False True True False False])
-    (Stringa.implode
-      [Stringa.Char False False True False False True True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char True False False False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char False False False True True True False False,
+        Str.Char True False True False True True False False,
+        Str.Char False True False False False True True False,
+        Str.Char False True False False False True True False,
+        Str.Char False True True False True True False False,
+        Str.Char True False True False True True False False])
+    (Str.implode
+      [Str.Char False False True False False True True False,
+        Str.Char True True True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char True False False False False True True False,
+        Str.Char False True False False True True True False]);
 
 dollarProvider :: SemanticsTypes.Party;
 dollarProvider =
   SemanticsTypes.Role
-    (Stringa.implode
-      [Stringa.Char False False True False False False True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char False False True True False True True False,
-        Stringa.Char True False False False False True True False,
-        Stringa.Char False True False False True True True False,
-        Stringa.Char False False False False False True False False,
-        Stringa.Char False False False False True False True False,
-        Stringa.Char False True False False True True True False,
-        Stringa.Char True True True True False True True False,
-        Stringa.Char False True True False True True True False,
-        Stringa.Char True False False True False True True False,
-        Stringa.Char False False True False False True True False,
-        Stringa.Char True False True False False True True False,
-        Stringa.Char False True False False True True True False]);
+    (Str.implode
+      [Str.Char False False True False False False True False,
+        Str.Char True True True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char False False True True False True True False,
+        Str.Char True False False False False True True False,
+        Str.Char False True False False True True True False,
+        Str.Char False False False False False True False False,
+        Str.Char False False False False True False True False,
+        Str.Char False True False False True True True False,
+        Str.Char True True True True False True True False,
+        Str.Char False True True False True True True False,
+        Str.Char True False False True False True True False,
+        Str.Char False False True False False True True False,
+        Str.Char True False True False False True True False,
+        Str.Char False True False False True True True False]);
 
 swapExample :: SemanticsTypes.Contract;
 swapExample =

isabelle/generated/Stringa.hs → isabelle/generated/Str.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}
 
-module Stringa(Char(..), implode) where {
+module Str(Char(..), implode) where {
 
 import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
   (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,

isabelle/marlowe.cabal

@@ -33,7 +33,7 @@ library
         Product_Lexorder
         Product_Type
         SList
-        Stringa
+        Str
     exposed-modules:
         Arith
         ArithNumInstance

nix/scripts.nix

@@ -37,4 +37,8 @@
     cd isabelle
     isabelle jedit -d . -u Doc/Specification/Specification.thy
   '';
+  vscode-marlowe-proofs = writeShellScriptBinInRepoRoot "vscode-marlowe-proofs" ''
+    cd isabelle
+    isabelle vscode  -o "editor_output_state=true" -d . -u Doc/Specification/Specification.thy .
+  '';
 }