From 114cae50a57b52ac143f1476bcea60f14928018e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Dec 2024 17:27:21 +0100 Subject: [PATCH] update gcm script Signed-off-by: Nikolaj Bjorner --- genaisrc/gcm.genai.mts | 113 ++++++++++++++++++++++++++++++-------- src/sat/smt/pb_solver.cpp | 44 +-------------- src/sat/smt/pb_solver.h | 1 - 3 files changed, 93 insertions(+), 65 deletions(-) diff --git a/genaisrc/gcm.genai.mts b/genaisrc/gcm.genai.mts index d1f97174f64..93e28e1d159 100644 --- a/genaisrc/gcm.genai.mts +++ b/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. + + : + + - can be one of the following: feat, fix, docs, style, refactor, perf, test, build, ci, chore, revert + - 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. + + : + + - can be one of the following: feat, fix, docs, style, refactor, perf, test, build, ci, chore, revert + - 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,14 +124,14 @@ 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 })) @@ -73,3 +139,4 @@ Please generate a concise, one-line commit message for these changes. break } } while (choice !== "commit") + diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index 496042f4916..b81c9d059f5 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/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: { diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h index 99ea459839e..8ef463dc311 100644 --- a/src/sat/smt/pb_solver.h +++ b/src/sat/smt/pb_solver.h @@ -332,7 +332,6 @@ namespace pb { constraint* active2card(); void active2wlits(); void active2wlits(svector& 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);