update gcm script

Signed-off-by: Nikolaj Bjorner <[email protected]>

genaisrc/gcm.genai.mts

@@ -1,6 +1,8 @@
 /**
- * git commit flow with auto-generated commit message
+ * Script to automate the git commit process with AI-generated commit messages.
+ * It checks for staged changes, generates a commit message, and prompts the user to review or edit the message before committing.
  */
+
 script({
     title: "git commit message",
     description: "Generate a commit message for all staged changes",
@@ -9,40 +11,104 @@ script({
 // Check for staged changes and stage all changes if none are staged
 const diff = await git.diff({
     staged: true,
-    excludedPaths: "**/genaiscript.d.ts",
     askStageOnEmpty: true,
 })
+
+// If no staged changes are found, cancel the script with a message
 if (!diff) cancel("no staged changes")
 
-// show diff in the console
+// Display the diff of staged changes in the console
 console.log(diff)
 
+// chunk if case of massive diff
+const chunks = await tokenizers.chunk(diff, { chunkSize: 10000 })
+if (chunks.length > 1)
+    console.log(`staged changes chunked into ${chunks.length} parts`)
+
 let choice
 let message
 do {
-    // Generate commit message
-    const res = await runPrompt(
-        (_) => {
-            _.def("GIT_DIFF", diff, { maxTokens: 20000 })
-            _.$`GIT_DIFF is a diff of all staged changes, coming from the command:
-\`\`\`
-git diff --cached
-\`\`\`
-Please generate a concise, one-line commit message for these changes.
-- do NOT add quotes
-` // TODO: add a better prompt
-        },
-        { cache: false, temperature: 0.8 }
-    )
-    if (res.error) throw res.error
+    // Generate a conventional commit message based on the staged changes diff
+    message = ""
+    for (const chunk of chunks) {
+        const res = await runPrompt(
+            (_) => {
+                _.def("GIT_DIFF", chunk, {
+                    maxTokens: 10000,
+                    language: "diff",
+                    detectPromptInjection: "available",
+                })
+                _.$`Generate a git conventional commit message that summarizes the changes in GIT_DIFF.
+
+        <type>: <description>
+
+        - <type> can be one of the following: feat, fix, docs, style, refactor, perf, test, build, ci, chore, revert
+        - <description> is a short, imperative present-tense description of the change
+        - GIT_DIFF is generated by "git diff"
+        - do NOT use markdown syntax
+        - do NOT add quotes, single quote or code blocks
+        - keep it short, 1 line only, maximum 50 characters
+        - follow the conventional commit spec at https://www.conventionalcommits.org/en/v1.0.0/#specification
+        - do NOT confuse delete lines starting with '-' and add lines starting with '+'
+        `
+            },
+            {
+                model: "large", // Specifies the LLM model to use for message generation
+                label: "generate commit message", // Label for the prompt task
+                system: [
+                    "system.assistant",
+                    "system.safety_jailbreak",
+                    "system.safety_harmful_content",
+                    "system.safety_validate_harmful_content",
+                ],
+            }
+        )
+        if (res.error) throw res.error
+        message += res.text + "\n"
+    }
 
-    message = res.text
+    // since we've concatenated the chunks, let's compress it back into a single sentence again
+    if (chunks.length > 1) {
+        const res =
+            await prompt`Generate a git conventional commit message that summarizes the COMMIT_MESSAGES.
+
+        <type>: <description>
+
+        - <type> can be one of the following: feat, fix, docs, style, refactor, perf, test, build, ci, chore, revert
+        - <description> is a short, imperative present-tense description of the change
+        - do NOT use markdown syntax
+        - do NOT add quotes or code blocks
+        - keep it short, 1 line only, maximum 50 characters
+        - use gitmoji
+        - follow the conventional commit spec at https://www.conventionalcommits.org/en/v1.0.0/#specification
+        - do NOT confuse delete lines starting with '-' and add lines starting with '+'
+        - do NOT respond anything else than the commit message
+
+        COMMIT_MESSAGES:
+        ${message}
+        `.options({
+                model: "large",
+                label: "summarize chunk commit messages",
+                system: [
+                    "system.assistant",
+                    "system.safety_jailbreak",
+                    "system.safety_harmful_content",
+                    "system.safety_validate_harmful_content",
+                ],
+            })
+        if (res.error) throw res.error
+        message = res.text
+    }
+
+    message = message?.trim()
     if (!message) {
-        console.log("No message generated, did you configure the LLM model?")
+        console.log(
+            "No commit message generated, did you configure the LLM model?"
+        )
         break
     }
 
-    // Prompt user for commit message
+    // Prompt user to accept, edit, or regenerate the commit message
     choice = await host.select(message, [
         {
             value: "commit",
@@ -58,18 +124,19 @@ Please generate a concise, one-line commit message for these changes.
         },
     ])
 
-    // Handle user choice
+    // Handle user's choice for commit message
     if (choice === "edit") {
         message = await host.input("Edit commit message", {
             required: true,
         })
         choice = "commit"
     }
-    // Regenerate message
+    // If user chooses to commit, execute the git commit and optionally push changes
     if (choice === "commit" && message) {
         console.log(await git.exec(["commit", "-m", message]))
         if (await host.confirm("Push changes?", { default: true }))
             console.log(await git.exec("push"))
         break
     }
 } while (choice !== "commit")
+

src/sat/smt/pb_solver.cpp

@@ -669,8 +669,6 @@ namespace pb {
             DEBUG_CODE(TRACE("sat_verbose", display(tout, m_A);););
             TRACE("pb", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";);
             SASSERT(offset > 0);
-
-            DEBUG_CODE(justification2pb(js, consequent, offset, m_B););
 
             if (_debug_conflict) {
                 IF_VERBOSE(0, 
@@ -713,12 +711,9 @@ namespace pb {
             case sat::justification::EXT_JUSTIFICATION: {
                 auto cindex = js.get_ext_justification_idx();
                 auto* ext = sat::constraint_base::to_extension(cindex);
-                if (ext != this) {
-                    m_lemma.reset();
-                    ext->get_antecedents(consequent, idx, m_lemma, false);
-                    for (literal l : m_lemma) process_antecedent(~l, offset);
-                    break;
-                }
+                if (ext != this) 
+                    return l_undef;
+
                 constraint& cnstr = index2constraint(cindex);
                 ++m_stats.m_num_resolves;
                 switch (cnstr.tag()) {
@@ -3442,39 +3437,6 @@ namespace pb {
         return c;
     }
 
-
-    void solver::justification2pb(sat::justification const& js, literal lit, unsigned offset, ineq& ineq) {
-        switch (js.get_kind()) {
-        case sat::justification::NONE:
-            SASSERT(lit != sat::null_literal);
-            ineq.reset(offset);
-            ineq.push(lit, offset);
-            break;
-        case sat::justification::BINARY:
-            SASSERT(lit != sat::null_literal);
-            ineq.reset(offset);
-            ineq.push(lit, offset);
-            ineq.push(js.get_literal(), offset);
-            break;
-        case sat::justification::CLAUSE: {
-            ineq.reset(offset);
-            sat::clause & c = s().get_clause(js);
-            for (literal l : c) ineq.push(l, offset);
-            break;
-        }
-        case sat::justification::EXT_JUSTIFICATION: {
-            sat::ext_justification_idx index = js.get_ext_justification_idx();
-            VERIFY(this == sat::constraint_base::to_extension(index));
-            constraint& cnstr = index2constraint(index);
-            constraint2pb(cnstr, lit, offset, ineq);
-            break;
-        }
-        default:
-            UNREACHABLE();
-            break;
-        }
-    }
-
     void solver::constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& ineq) {
         switch (cnstr.tag()) {
         case pb::tag_t::card_t: {

src/sat/smt/pb_solver.h

@@ -332,7 +332,6 @@ namespace pb {
         constraint* active2card();
         void active2wlits();
         void active2wlits(svector<wliteral>& wlits);
-        void justification2pb(sat::justification const& j, literal lit, unsigned offset, ineq& p);
         void constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& p);
         bool validate_resolvent();
         unsigned get_coeff(ineq const& pb, literal lit);