1 release 1 tag

RSS feed

• v0.1.0 5524b33686

  Compare

  v0.1.0 Stable

  marfavi released this 2026-10-30 15:08:21 +01:00 | 0 commits to main since this release

  First alpha release. Supported platforms are macOS on Apple Silicon
  (darwin-arm64), Linux x64 (linux-x64) and Linux arm64 (linux-arm64).

  Added

  • Diagnostics and theme-aware syntax highlighting for
    /*@ ... */ annotations in C files.
  • Navigation between annotations and their Rocq definitions and proofs, in both
    directions.
  • Rocq model generation with clightgen, model-staleness tracking and a
    .crocqcache workspace cache.
  • Dependency checks for Rocq, CompCert/clightgen and VsRocq, with a status bar
    chip and Dependencies/Rocq model views.
  • Proof-file scaffolding from templates, including an explicit overwrite
    variant.
  • Annotation formatting, manually or on save.
  • Inline SPEC_INLINE/INV_INLINE clause bodies that are written into the
    linked Rocq definitions when the C file is saved.

  Known issues

  • Windows is not supported in this release. Intel macOS is also unsupported.
  • Generated proof documents contain placeholder specifications and invariants
    and do not compile until they are filled in.
  • Editing a .v definition that an inline clause owns is overwritten when the C
    file is saved.
  • Some Rocq documents can surface VsRocq/Rocq errors when opened.
  • Proof status (solved/admitted) and code completions are not implemented yet.

  Downloads

  • crocq-0.1.0.vsix
    0 downloads · 2026-10-30 15:17:50 +01:00 · 1.7 MiB
  • crocq-0.1.0.vsix.sha256
    0 downloads · 2026-10-30 15:17:51 +01:00 · 85 B

  ---

  • Source code (ZIP)
    0 downloads
  • Source code (TAR.GZ)
    0 downloads