simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 08:54:24 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 60dae8cd1f real proof production for CC simon/emit-talweg-proof Simon Cruanes 2026-05-04 22:42:55 -04:00
  • 62422169ea fix qcheck deprecation warnings Simon Cruanes 2026-05-03 23:01:35 -04:00
  • 4c4ff26d07 remove dead script Simon Cruanes 2026-05-03 22:45:51 -04:00
  • 969a04f630 make format + ignore generated .granite files Simon Cruanes 2026-05-03 21:28:31 +00:00
  • 3932c247d4 proof: eliminate P_let/P_local; emit subproofs eagerly via tracer Simon Cruanes 2026-05-03 20:30:58 +00:00
  • 62f88df1f4 add minidag proof emitter; wire as default tracer replacing bencode Simon Cruanes 2026-05-03 19:32:11 +00:00
  • aa53ae601a port minidag encode/decode from granite (encoding part only) Simon Cruanes 2026-05-03 19:18:37 +00:00
  • e2990469fe add benchpress.lua simon/benchpress-lua Simon Cruanes 2026-05-01 22:35:05 -04:00
  • 1971d2a8e8 test config main Simon Cruanes 2026-04-24 21:12:12 -04:00
  • c295d22921 bump min version for smtlib-utils Simon Cruanes 2026-04-24 01:03:00 -04:00
  • 94f178d400 makefile Simon Cruanes 2026-04-24 00:55:55 -04:00
  • 701f18561a gitignore Simon Cruanes 2026-04-23 22:36:45 -04:00
  • 0c965aec23 proof export into talweg text format Simon Cruanes 2026-03-16 04:17:39 +00:00
  • 990a1e6f69 format Simon Cruanes 2026-03-16 03:01:15 +00:00
  • d9a0b66973 fix warnings Simon Cruanes 2026-03-16 03:01:09 +00:00
  • 491f368142 gitignore Simon Cruanes 2026-03-14 23:48:52 -04:00
  • 26d58218d4 sample lia problems Simon Cruanes 2026-03-14 23:48:45 -04:00
  • 1daf8d6fed
         delete plugin Simon Cruanes 2026-03-19 00:22:55 -04:00
  • f7a04f1f93 fix compilation error Simon Cruanes 2026-03-19 03:35:26 +00:00
  • 5fcbaaacac ocamlformat 0.27 Simon Cruanes 2026-03-19 03:27:48 +00:00
  • fd50e0a34b remove specialized vectors, keep only Vec Simon Cruanes 2026-03-19 03:27:23 +00:00
  • 08b3da6931 reformat dune files Simon Cruanes 2026-03-19 03:26:39 +00:00
  • d5a7ff4c46
         gitignore wip-levels-in-kernel Simon Cruanes 2026-03-15 00:33:42 -04:00
  • 6fb4f7efe0 improve leancheck to handle #def Simon Cruanes 2026-03-15 04:35:59 +00:00
  • 588c128a55 makefile Simon Cruanes 2026-03-15 04:27:58 +00:00
  • c5e7c11131 ocamlformat config Simon Cruanes 2026-03-15 04:27:52 +00:00
  • 93f3964d11 update ciclib+format Simon Cruanes 2026-03-15 04:27:32 +00:00
  • 7f96ed239d update leancheck+format Simon Cruanes 2026-03-15 04:27:25 +00:00
  • 08a7b7a3fd core-logic: format Simon Cruanes 2026-03-15 04:27:06 +00:00
  • 37411ed50f core-logic: add def_eq + whnf Simon Cruanes 2026-03-15 04:24:54 +00:00
  • 98128717df refactor: Rrplace Veci and Vec_float with polymorphic Vec Simon Cruanes 2026-03-11 03:28:28 -04:00
  • fcbaaae81d Vec: fix bound check error Simon Cruanes 2026-03-11 03:26:57 -04:00
  • 14a7e16925 Add symlink to main executable Simon Cruanes 2026-02-08 02:20:31 +00:00
  • 1530b761b0
         wip: leancheck Simon Cruanes 2023-04-20 22:05:15 -04:00
  • 8d70c10e18
         wip: ciclib: start checking types and inductive specs Simon Cruanes 2023-03-07 23:38:31 -05:00
  • 401365e1bb
         fix Simon Cruanes 2023-03-06 23:42:37 -05:00
  • 42c6d2f770
         ciclib: beta-reduction Simon Cruanes 2023-03-06 23:38:00 -05:00
  • 6fee09848b
         leancheck: parse ind Simon Cruanes 2023-03-06 21:51:13 -05:00
  • 38133dc163
         wip: leancheck: use colors, better debug Simon Cruanes 2023-03-06 20:50:44 -05:00
  • 8f02f14d37
         feat(leancheck): handle term constructors Simon Cruanes 2023-03-05 23:08:38 -05:00
  • 0d948a9324
         feat(ciclib): adapt AST to be closer to lean proof format Simon Cruanes 2023-03-05 23:08:24 -05:00
  • b1aaff4e9f
         feat: add sidekick.cic_lib with non-hashconsed terms Simon Cruanes 2023-03-04 23:30:18 -05:00
  • a8f69a834f
         wip: feat(leancheck): parse universe commands Simon Cruanes 2023-03-02 00:07:20 -05:00
  • 75e42072f4
         wip: feat(leancheck): store intermediate objects of the proof Simon Cruanes 2023-03-01 22:37:04 -05:00
  • 39aa3d7f64
         feat(level): more judgements Simon Cruanes 2023-03-01 22:36:56 -05:00
  • 2c435a5c18
         fix(level): missing cases, inspiration from Trepplein Simon Cruanes 2023-03-01 22:16:58 -05:00
  • cd07d6924b
         details for leancheck Simon Cruanes 2023-02-28 23:38:04 -05:00
  • 70f0b3874c
         wip: feat(leancheck): start binary to check lean proofs Simon Cruanes 2023-02-28 23:28:12 -05:00
  • 0b51dd172e
         feat(level): implement level comparison Simon Cruanes 2023-02-28 22:38:12 -05:00
  • 1eeb5a464d
         test: update test with levels Simon Cruanes 2023-02-23 22:08:50 -05:00
  • 9ea96a6b61
         refactor: adapt to new levels in core Simon Cruanes 2023-02-23 22:07:55 -05:00
  • b8cbe0cf06
         feat(core-logic): add level expressions, modify type checker Simon Cruanes 2023-02-23 22:07:34 -05:00
  • 4363fc47b6
         update smtlib Simon Cruanes 2025-01-27 21:51:51 -05:00
  • 6c8d6840f8
         chore: update workflows Simon Cruanes 2025-01-27 21:49:09 -05:00
  • 90a5c7bc06
         ocamlforamt Simon Cruanes 2025-01-27 21:49:05 -05:00
  • 8e6036bf3f
         chore: CI Simon Cruanes 2023-12-27 19:38:24 -05:00
  • 13440d60f6
         chore: CI Simon Cruanes 2023-12-27 19:31:55 -05:00
  • 2c7065e7fd deploy: eff6016151 gh-pages c-cube 2023-12-27 22:31:52 +00:00
  • eff6016151
         support trace-fuchsia if present master Simon Cruanes 2023-12-27 17:24:35 -05:00
  • 54077446ca
         require ocaml 4.08, compat with containers 3.13 Simon Cruanes 2023-12-07 00:14:16 -05:00
  • aeb7ff8b4f deploy: 85c39d3642 c-cube 2023-12-07 05:10:29 +00:00
  • 85c39d3642
         faster CI Simon Cruanes 2023-12-07 00:03:36 -05:00
  • a3e9ecf974 deploy: 43c8e60790 c-cube 2023-10-07 02:14:09 +00:00
  • 43c8e60790
         use trace instead of our own custom tracing setup Simon Cruanes 2023-10-06 22:04:15 -04:00
  • 4bb15f8b5e
         comments Simon Cruanes 2023-10-06 21:35:23 -04:00
  • c35d721c6d fix: compute model even if (potentially) new interface eqns are produced Simon Cruanes 2023-06-23 10:44:12 -04:00
  • da5cd7fbc2
         fix: compute model even if (potentially) new interface eqns are produced wip-19 Simon Cruanes 2023-06-23 10:44:12 -04:00
  • 088fe6e281 deploy: 3ebc532486 c-cube 2023-06-26 19:47:10 +00:00
  • 3ebc532486 more tests Simon Cruanes 2023-06-26 00:44:51 -04:00
  • 923cbec6e5 remove debug msg Simon Cruanes 2023-06-26 00:40:39 -04:00
  • 8d8ef4211b fix sign error Simon Cruanes 2023-06-26 00:40:31 -04:00
  • 67e9eabf43 add another bug repro Simon Cruanes 2023-06-25 15:39:28 -04:00
  • 477c780f18 CI Simon Cruanes 2023-06-23 21:42:43 -04:00
  • d8612f84c9 doc Simon Cruanes 2023-06-23 21:39:58 -04:00
  • 2e29ab20dd fix benchpress config Simon Cruanes 2023-06-23 21:26:55 -04:00
  • 3ba2583966 fix lra: define expressions occurring in subterms properly Simon Cruanes 2023-06-23 21:23:50 -04:00
  • c4d3c44c49 warnings and comments Simon Cruanes 2023-06-23 21:23:42 -04:00
  • c64bebaf6f fix warning Simon Cruanes 2023-06-23 21:22:55 -04:00
  • dcdc55ee1f add non reduced test too Simon Cruanes 2023-06-23 17:20:39 -04:00
  • 87f9be7fe0 test: add regression test for LRA bug Simon Cruanes 2023-06-23 15:54:06 -04:00
  • 7937a38416
         more tests Simon Cruanes 2023-06-26 00:44:51 -04:00
  • 55b2fa00f4
         remove debug msg Simon Cruanes 2023-06-26 00:40:39 -04:00
  • 5d07d456dc
         fix sign error Simon Cruanes 2023-06-26 00:40:31 -04:00
  • 0841e0e767
         add another bug repro Simon Cruanes 2023-06-25 15:39:28 -04:00
  • 3b78fdda87
         CI Simon Cruanes 2023-06-23 21:42:43 -04:00
  • 1d1fc88f1c
         doc Simon Cruanes 2023-06-23 21:39:58 -04:00
  • 66a155a155 deploy: 619da6fbcb c-cube 2023-06-24 01:36:40 +00:00
  • 27937b664a
         fix benchpress config Simon Cruanes 2023-06-23 21:26:55 -04:00
  • a767ca1603
         fix lra: define expressions occurring in subterms properly Simon Cruanes 2023-06-23 21:23:50 -04:00
  • 68c4acde4e
         warnings and comments Simon Cruanes 2023-06-23 21:23:42 -04:00
  • 1fe814a046
         fix warning Simon Cruanes 2023-06-23 21:22:55 -04:00
  • 0b80cdb1dc
         add non reduced test too Simon Cruanes 2023-06-23 17:20:39 -04:00
  • 4be08675a1
         test: add regression test for LRA bug Simon Cruanes 2023-06-23 15:54:06 -04:00
  • 619da6fbcb
         fix warnings Simon Cruanes 2023-06-23 20:44:01 -04:00
  • 0393fae090
         cdsat wip-ccsat Simon Cruanes 2023-05-09 20:42:24 -04:00
  • 8fbfa98fc8
         wip: union find in ccsat Simon Cruanes 2023-05-09 20:42:12 -04:00
  • 566d0d64a2
         detail wip-cdsat Simon Cruanes 2022-11-16 22:30:54 -05:00
  • f2a7489d39
         feat(cdsat): decide new variables Simon Cruanes 2022-11-06 22:37:10 -05:00
  • 3412b272fb
         fix(tvar): remove redundant has_value bitvec Simon Cruanes 2022-11-08 11:46:46 -05:00
  • 1153c21a52
         feat(cdsat): add variables (to plugins, to-decide set) Simon Cruanes 2022-11-08 11:43:38 -05:00