All pull requests

Pull requests

• CI(windows): install opam depexts from pwsh

  #4831·gebner opened Nov 3, 2026Contributor·

  ·

• Do not normalize erased spec arguments during extraction

  #4830·gebner opened Nov 3, 2026Contributor·

  ·
  1

• Custard: add opt-in function-level C local declaration hoisting

  #4820·tahina-pro opened Nov 2, 2026Member·

  ·
  1

• Pulse: library-only logical atomicity with helping and FIFO examples

  #4806·nikswamy opened Oct 28, 2026Contributor·

  ·
  2

• Pulse: verified effect libraries and native exception checking

  #4798·nikswamy opened Oct 26, 2026Contributor·

  ·

• Hierarchical modules: IDE / file name fix

  #4797·amosr-msft opened Oct 26, 2026Contributor·

  ·
  6

• CI: run the compiler's unit tests compiled with Cherry

  #4764·gebner opened Oct 22, 2026Contributor·

  ·

• Add SMT encoding sharing (WIP!)

  #4760·amosr-msft opened Oct 22, 2026Contributor·

  ·
  4

• Env: memoize all_binders with the gamma it was built for

  #4687·nikswamy opened Oct 16, 2026Contributor·

  ·
  3

• SMTEncoding: --ext smt_squash_binders states squash binders as their facts

  #4684·nikswamy opened Oct 16, 2026Contributor·

  ·
  1

• SMTEncoding: discharge split goals that are literally a hypothesis

  #4683·nikswamy opened Oct 16, 2026Contributor·

  ·

• SMTEncoding: memoize normalized local sorts in env_t

  #4682·nikswamy opened Oct 16, 2026Contributor·

  ·
  5

• Add structured documentation support (experimental)

  #4657·kapilash opened Oct 9, 2026·

  ·
  2

• Use the Core typechecker as F*'s only VC generator; Rel computes no guards

  #4605·nikswamy opened Sep 26, 2026Contributor·

  ·
  3

  15

• SMT: state ground typing facts for refined pure applications (#4591)

  #4602·gebner opened Sep 25, 2026Contributor·

  ·
  1

  2

• Restate quantifier-free argument refinements at lemma calls (fixes #4591)

  #4597·gebner opened Sep 24, 2026Contributor·

  ·
  1

  2

• Batch tactic proof obligations that share a context into one SMT query

  #4557·gebner opened Sep 22, 2026Contributor·

  ·
  3

• SMT encoding: eliminate unit-refinement binders in favor of implications

  #4524·gebner opened Sep 3, 2026Contributor·

  ·
  4

• Eta-expand product-typed holes in Pulse

  #4497·hei411 opened Aug 27, 2026Collaborator·

  ·
  1

• Pulse: only drop leaked branch refinements, fixing #4488 rlimit regression

  #4496·gebner opened Aug 27, 2026Contributor·

  ·
  1

• tools/depgraph

  #4464·nikswamy opened Aug 22, 2026Contributor·

  ·
  1

• Pulse: purify stateful-read sugar in call arguments (fixes #4423)

  #4424·hei411 opened Aug 12, 2026Collaborator·

  ·
  1

  3

• Change book's LaTeX engine to XeLaTex

  #4413·smheidrich opened Aug 10, 2026Contributor·

  ·

• Mention Unicode forms of syntax elements in book

  #4412·smheidrich opened Aug 10, 2026Contributor·

  ·
  1

  1

• Differential tests and patches to NBE to match its behavior with the normalizer

  #4398·nikswamy opened Aug 7, 2026Contributor·

  ·