Skip to content

Actions: rocq-prover/rocq

Actions

Github CI

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
ci-github.yml
2,500+ workflow runs
2,500+ workflow runs

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
Simpler implementation of undefined_evars_cache Github CI #4439: Pull request #21984 synchronize by SkySkimmer
In progress SkySkimmer:evar-cache
SkySkimmer:evar-cache
In progress
Merge PR #21982: Remove Context.Compacted.Declaration.to_named_context Github CI #4438: Commit fc4dbca pushed by coqbot-app Bot
In progress master
master
In progress
Keep track of which variables are section variables and use this info to fix bugs Github CI #4437: Pull request #21987 synchronize by SkySkimmer
In progress SkySkimmer:context-secvar
SkySkimmer:context-secvar
In progress
Inline canonical equality in kernel subtyping. Github CI #4436: Pull request #21998 opened by ppedrot
35m 37s ppedrot:kernel-subtype-canord-inline
ppedrot:kernel-subtype-canord-inline
35m 37s
Merge PR #21950: Create rocq doc backend for Alectryon Github CI #4435: Commit 7f41334 pushed by coqbot-app Bot
12m 25s master
master
12m 25s
Merge PR #21993: Deprecate the GlobRef.Map module. Github CI #4434: Commit 2cb9b48 pushed by coqbot-app Bot
20s master
master
20s
TC search: log hint before hint is applied Github CI #4433: Pull request #21899 synchronize by Janno
35m 42s Janno:janno/typeclasses-debug
Janno:janno/typeclasses-debug
35m 42s
TC search: log hint before hint is applied Github CI #4432: Pull request #21899 synchronize by Janno
34m 36s Janno:janno/typeclasses-debug
Janno:janno/typeclasses-debug
34m 36s
Merge PR #21994: Minor code factorization in Declareops. Github CI #4431: Commit 0a16eef pushed by coqbot-app Bot
35m 16s master
master
35m 16s
TC search: log hint before hint is applied Github CI #4430: Pull request #21899 synchronize by Janno
36m 29s Janno:janno/typeclasses-debug
Janno:janno/typeclasses-debug
36m 29s
Strict Resolution has precedence over Hint Mode Github CI #4429: Pull request #21997 opened by Janno
35m 24s Janno:janno/hint-mode-i
Janno:janno/hint-mode-i
35m 24s
[experiment] Convert stack in the right order except for application nodes. Github CI #4428: Pull request #21996 opened by ppedrot
35m 7s ppedrot:conversion-right-order-except-application
ppedrot:conversion-right-order-except-application
35m 7s
Minor code factorization in Declareops. Github CI #4427: Pull request #21994 opened by ppedrot
37m 16s ppedrot:declareops-factor-recarg-equality
ppedrot:declareops-factor-recarg-equality
37m 16s
Deprecate the GlobRef.Map module. Github CI #4426: Pull request #21993 opened by ppedrot
35m 23s ppedrot:deprecate-globrefmap
ppedrot:deprecate-globrefmap
35m 23s
Merge PR #21986: Stop relying on canonizing GlobRef.Map in hint inter… Github CI #4425: Commit df88c3c pushed by coqbot-app Bot
36m 45s master
master
36m 45s
Merge PR #21981: Rely on user-facing names for rocqchk opaque analysis. Github CI #4424: Commit 9bef87f pushed by coqbot-app Bot
1m 31s master
master
1m 31s
Merge PR #21985: Stop relying on canonical equality in Inductiveops. Github CI #4423: Commit 7f472df pushed by coqbot-app Bot
20s master
master
20s
Ltac2 share some code between lazy_match and multi_match Github CI #4422: Pull request #21992 opened by SkySkimmer
33m 51s SkySkimmer:patte-mat
SkySkimmer:patte-mat
33m 51s
Merge PR #21990: rocqide get background goals when needed Github CI #4421: Commit f6f6116 pushed by coqbot-app Bot
33m 6s master
master
33m 6s
Merge PR #21988: rocqide -xml-debug does not imply -debug Github CI #4420: Commit 46e8103 pushed by coqbot-app Bot
18s master
master
18s
Merge PR #21991: Inline some constant arguments in rocqide Github CI #4419: Commit f8ec577 pushed by coqbot-app Bot
33m 59s master
master
33m 59s
Inline some constant arguments in rocqide Github CI #4418: Pull request #21991 opened by SkySkimmer
35m 44s SkySkimmer:ide-cfold
SkySkimmer:ide-cfold
35m 44s
rocqide get background goals when needed Github CI #4417: Pull request #21990 opened by SkySkimmer
35m 43s SkySkimmer:bg-goals
SkySkimmer:bg-goals
35m 43s
rocqide -xml-debug does not imply -debug Github CI #4416: Pull request #21988 opened by SkySkimmer
37m 5s SkySkimmer:xml-debug
SkySkimmer:xml-debug
37m 5s
Merge PR #21973: Clean up function CClosure.get_branch Github CI #4415: Commit 2f4c858 pushed by coqbot-app Bot
37m 0s master
master
37m 0s