Skip to content

Show tactics proposed by the remote agent#248

Closed
ehtesham-zahoor wants to merge 1 commit intomainfrom
fix/remote-agent-status-updates
Closed

Show tactics proposed by the remote agent#248
ehtesham-zahoor wants to merge 1 commit intomainfrom
fix/remote-agent-status-updates

Conversation

@ehtesham-zahoor
Copy link
Copy Markdown
Contributor

@ehtesham-zahoor ehtesham-zahoor commented Feb 24, 2026

In the long run, we need more status message from the remote agent but currently showing the tactics being proposed seems sufficient.

Running the proving agent.

Found admit at index 8.
Goal 0:
  ============================
  forall a : my_nat, my_add MyO a = a


#[local] Unset SsrIdents.
#[local] Set Default Goal Selector "1".
verify_spec; go.
intros a.
simpl.
reflexivity.
Qed.
Agent succeeded.

@ehtesham-zahoor
Copy link
Copy Markdown
Contributor Author

@sky-rayan

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Feb 24, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ fix/remote-agent-status-updates 7f875ae 2a21066 #248

Passive Repos

Repo Job Branch Job Commit
./ main 57d9592
fmdeps/BRiCk/ main f324984
fmdeps/auto/ main b5395a0
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 0c0b4de
bluerock/bhv/ skylabs-main 5a39ba2
fmdeps/brick-libcpp/ main 53842f7
fmdeps/ci/ main d406d7d
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 46ed5a6
psi/protos/ main 8fe3e7c
psi/backend/ main 37f7734
psi/ide/ main 6b596cf
psi/data/ main 6c7fffd
vendored/rocq/ skylabs-master 2ede3c9
vendored/rocq-elpi/ skylabs-master 103a742
vendored/rocq-equations/ skylabs-main a8c4832
vendored/rocq-ext-lib/ skylabs-master 94a6630
vendored/rocq-iris/ skylabs-master 3ad4ddd
vendored/rocq-lsp/ skylabs-main a8b7272
vendored/rocq-stdlib/ skylabs-master bc07423
vendored/rocq-stdpp/ skylabs-master e01d802
fmdeps/skylabs-fm/ main 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122640.9 122640.9 -0.0 total
-0.00% 22464.3 22464.3 -0.0 ├ translation units
+0.00% 100176.6 100176.6 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122640.9 122640.9 -0.0 total
-0.00% 22464.3 22464.3 -0.0 ├ translation units
+0.00% 100176.6 100176.6 +0.0 └ proofs and tests

@ehtesham-zahoor
Copy link
Copy Markdown
Contributor Author

closing this in favor of #254

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant