experiment

2024/02/01/notes.org

@@ -0,0 +1,8 @@
+
+*  run the script
+run20.sh to run 20 iterations over the task.
+
+it expects ~/experiments/lang_agent/_build/default/bin/worker.exe to be where you built the
+https://github.com/meta-introspector/lang_agent and
+~/experiments/lang_agent/huggingface/ to be where we write the data
+https://huggingface.co/datasets/introspector/unimath/

2024/02/01/notes.org~

@@ -0,0 +1 @@
+

2024/02/01/prompt.txt

@@ -0,0 +1,11 @@
+
+use coq proof traces to create workflows for ai agent
+   (lang_agent ocaml +ollama,)
+ introspector and user intefaces and openapi apis.
+
+We are going on a journey to convert unimath, the modern homotopy system into a comic book form preserving its main information and mapping each part of it into art that contains the math and can be reinterpreted if you have the key.
+We want to convert unimath into a series of zero knowledge proof snarks that extract interesting properties about the system that only an expert would know. 
+split up this following text into logical	 chunks for each snark.
+Use creativity. Create a screenplay for a explainer youtube video like 3b1b. Invoke the muses, and ask each one in turn to bless your endevour. Ask Athena for wisdom. Ask Mars for courage. Use all of this to create a wonderful interpretation of the following math code in coq.
+
+ Here is an example proof trace file from unimath that we can annotate with source and feed to the llm as well. so the idea is read the source and the proof traces and eventually use the proof traces as workflows for the llm to follow.

2024/02/01/run20.sh

@@ -0,0 +1,2 @@
+for x in {1..20}; do echo $x;
+		     bash -x ./test.sh $x;  done

2024/02/01/run20.sh~

@@ -0,0 +1 @@
+for x in {1..20}; do echo $x; bash ./test.sh $x;  done

2024/02/01/separator.txt

@@ -0,0 +1,3 @@
+
+#+end_src input
+Your response:

2024/02/01/task.txt

@@ -0,0 +1,168 @@
+ ulimit -v unlimited ; make -f build/CoqMakefile.make all
+make[1]: Entering directory '/mnt/data1/2024/01/05/UniMath'
+COQDEP VFILES
+COQC UniMath/CategoryTheory/limits/Examples/UnitCategoryLimits.v
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+simple_rapply p
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+fun p =>
+  simple refine p ||
+    simple refine (p _) ||
+      simple refine (p _ _) ||
+...
+simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+                               || simple refine
+                               (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+
+TcDebug (1) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+simple refine p ||
+  simple refine (p _) ||
+    simple refine (p _ _) ||
+...
+simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+
+TcDebug (1) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+simple refine p
+Level 1: evaluation returns
+simple refine p ||
+  simple refine (p _) ||
+...
+simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+where
+p := make_isTerminal
+of type
+uconstr of type tacvalue
+
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+<coq-core.plugins.ltac::simple_refine@0> $1
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+simple refine (p _) ||
+  simple refine (p _ _) ||
+  ...
+  simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+Level 0: In environment
+x : unit_category
+The term "make_isTerminal" has type
+ "∏ b : unit_category,
+  (∏ a : unit_category, iscontr (unit_category ⟦ a, b ⟧))
+  → isTerminal unit_category b" while it is expected to have type
+ "isTerminal unit_category x"
+(cannot unify "(∏ a : unit_category, iscontr (unit_category ⟦ a, b ⟧))
+               → isTerminal unit_category b" and
+"iscontr (unit_category ⟦ b, x ⟧)").
+Level 0: In environment
+x : unit_category
+The term "make_isTerminal" has type
+ "∏ b : unit_category,
+  (∏ a : unit_category, iscontr (unit_category ⟦ a, b ⟧))
+  → isTerminal unit_category b" while it is expected to have type
+ "isTerminal unit_category x"
+(cannot unify "(∏ a : unit_category, iscontr (unit_category ⟦ a, b ⟧))
+               → isTerminal unit_category b" and
+"iscontr (unit_category ⟦ b, x ⟧)").
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+simple refine (p _)
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+<coq-core.plugins.ltac::simple_refine@0> $1
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+simple refine (p _ _) ||
+  simple refine (p _ _ _) ||
+    simple refine (p _ _ _ _) ||
+...
+                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+Level 0: In environment
+x : unit_category
+The term "make_isTerminal ?b" has type
+ "(∏ a : ?C, iscontr (?C ⟦ a, ?b ⟧)) → isTerminal ?C ?b"
+while it is expected to have type "isTerminal unit_category x".
+Level 0: In environment
+x : unit_category
+The term "make_isTerminal ?b" has type
+ "(∏ a : ?C, iscontr (?C ⟦ a, ?b ⟧)) → isTerminal ?C ?b"
+while it is expected to have type "isTerminal unit_category x".
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+
+
+Going to execute:
+simple refine (p _ _)
+
+TcDebug (0) > 
+Goal:
+    x : ob unit_category
+  ============================
+   (isTerminal unit_category x)
+