Build documentation

Workflow runs for Build documentation

• [documentation]: document seq tactic

  completed successfully:
  Build documentation#1627:Commit5ffc8ffpushedbygithub-merge-queue[bot]Bot
  main

  Oct 30, 20267m 35s
  More actions for workflow run 1627

• remove parts that are in flux (or might be wrong) due to soundness fixes

  completed successfully:
  Build documentation#1626:Commitc37f918pushedbyfdupress
  main

  Oct 30, 20267m 51s
  More actions for workflow run 1626

• fix(phl): require the invariant on loop entry in the while variant …

  completed successfully:
  Build documentation#1625:Commit21d1f1epushedbygithub-merge-queue[bot]Bot
  main

  Oct 30, 20265m 53s
  More actions for workflow run 1625

• [documentation]: document while tactic

  completed successfully:
  Build documentation#1624:Pull request#880synchronizebyfdupress
  doc-while-tactic

  Oct 30, 202612m 54s
  More actions for workflow run 1624

• [documentation]: document seq tactic

  completed successfully:
  Build documentation#1623:Pull request#879synchronizebyfdupress
  doc-seq-tactic

  Oct 30, 20267m 37s
  More actions for workflow run 1623

• [documentation]: document seq tactic

  cancelled:
  Build documentation#1622:Pull request#879synchronizebyfdupress
  doc-seq-tactic

  Oct 30, 20262m 7s
  More actions for workflow run 1622

• [docker] bump z3 5.3.2 to 5.3.3

  completed successfully:
  Build documentation#1621:Commit76d5c0dpushedbyfdupress
  main

  Oct 30, 20268m 5s
  More actions for workflow run 1621

• [docker] bump z3 5.3.2 to 5.3.3

  completed successfully:
  Build documentation#1620:Pull request#1225openedbyfdupress
  docker-z3-5.3.3

  Oct 30, 202610m 41s
  More actions for workflow run 1620

• feat(theories): make FinType.card abstract, specified by card_spec

  requires action with the application:
  Build documentation#1619:Pull request#1224openedbymattc-try
  mattc-try:feat/fintype-abstract-card

  Oct 30, 2026Action required
  More actions for workflow run 1619

• fix(phl): require the invariant on loop entry in the while variant rule

  completed successfully:
  Build documentation#1618:Pull request#1132synchronizebyYiping106283
  Yiping106283:fix-phoare-while-variant-entry

  Oct 30, 202614m 58s
  More actions for workflow run 1618

• fix(phl): check the bound of the upper-bound while rule on all memories

  completed successfully:
  Build documentation#1617:Pull request#1130synchronizebyYiping106283
  Yiping106283:fix-phoare-while-le-bound

  Oct 30, 20267m 22s
  More actions for workflow run 1617

• fix(fixpoint): matchfix termination check must descend into all call …

  completed successfully:
  Build documentation#1616:Commit9eac73fpushedbygithub-merge-queue[bot]Bot
  main

  Oct 29, 20266m 35s
  More actions for workflow run 1616

• fix(sim): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

  completed successfully:
  Build documentation#1615:Pull request#1143synchronizebynamasikanam
  fix/eqobs-abs-oracle-glob

  Oct 29, 20267m 20s
  More actions for workflow run 1615

• upgrade to why3 1.9.0

  completed successfully:
  Build documentation#1614:Commit1445c70pushedbygithub-merge-queue[bot]Bot
  main

  Oct 28, 20265m 37s
  More actions for workflow run 1614

• upgrade to why3 1.9.0

  completed successfully:
  Build documentation#1613:Pull request#1220synchronizebystrub
  why3-1.9

  Oct 28, 202610m 59s
  More actions for workflow run 1613

• upgrade to why3 1.9.0

  cancelled:
  Build documentation#1612:Pull request#1220synchronizebystrub
  why3-1.9

  Oct 28, 20261m 10s
  More actions for workflow run 1612

• perf(smt): no relevance tables when no lemma is to be selected

  completed successfully:
  Build documentation#1611:Commit7bbf3b0pushedbystrub
  main

  Oct 28, 20267m 54s
  More actions for workflow run 1611

• fix(fixpoint): matchfix termination check must descend into all call arguments

  completed successfully:
  Build documentation#1610:Pull request#1144synchronizebynamasikanam
  fix/matchfix-sibling-arg-termination

  Oct 28, 20266m 9s
  More actions for workflow run 1610

• perf(smt): no relevance tables when no lemma is to be selected

  completed successfully:
  Build documentation#1609:Pull request#1221synchronizebystrub
  perf/smt-given-lemmas

  Oct 28, 20267m 32s
  More actions for workflow run 1609

• perf(smt): no relevance tables when no lemma is to be selected

  completed successfully:
  Build documentation#1608:Pull request#1221synchronizebystrub
  perf/smt-given-lemmas

  Oct 28, 202613m 26s
  More actions for workflow run 1608

• perf(smt): memories as abstract values, local variables as functions …

  completed successfully:
  Build documentation#1607:Commitc105190pushedbystrub
  main

  Oct 28, 20267m 48s
  More actions for workflow run 1607

• perf(smt): memories as abstract values, local variables as functions of them

  completed successfully:
  Build documentation#1606:Pull request#1222synchronizebystrub
  perf/smt-memory-locals

  Oct 28, 20267m 52s
  More actions for workflow run 1606

• perf(smt): memories as abstract values, local variables as functions of them

  completed successfully:
  Build documentation#1605:Pull request#1222synchronizebystrub
  perf/smt-memory-locals

  Oct 28, 20267m 7s
  More actions for workflow run 1605

• perf(smt): memories as abstract values, local variables as functions of them

  completed successfully:
  Build documentation#1604:Pull request#1222openedbystrub
  perf/smt-memory-locals

  Oct 28, 20266m 15s
  More actions for workflow run 1604

• upgrade to why3 1.9.0

  completed successfully:
  Build documentation#1603:Pull request#1220synchronizebyfdupress
  why3-1.9

  Oct 28, 20267m 57s
  More actions for workflow run 1603