1952 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Simon Cruanes	1530b761b0	wip: leancheck	2025-01-27 21:52:00 -05:00
Simon Cruanes	8d70c10e18	wip: ciclib: start checking types and inductive specs	2025-01-27 21:52:00 -05:00
Simon Cruanes	401365e1bb	fix	2025-01-27 21:52:00 -05:00
Simon Cruanes	42c6d2f770	ciclib: beta-reduction	2025-01-27 21:52:00 -05:00
Simon Cruanes	6fee09848b	leancheck: parse ind	2025-01-27 21:52:00 -05:00
Simon Cruanes	38133dc163	wip: leancheck: use colors, better debug	2025-01-27 21:52:00 -05:00
Simon Cruanes	8f02f14d37	feat(leancheck): handle term constructors	2025-01-27 21:52:00 -05:00
Simon Cruanes	0d948a9324	feat(ciclib): adapt AST to be closer to lean proof format	2025-01-27 21:52:00 -05:00
Simon Cruanes	b1aaff4e9f	feat: add sidekick.cic_lib with non-hashconsed terms ... this should be lighter and closer to Lean's proof format, where terms don't carry their type, and DB indices are not typed except from the context.	2025-01-27 21:52:00 -05:00
Simon Cruanes	a8f69a834f	wip: feat(leancheck): parse universe commands	2025-01-27 21:52:00 -05:00
Simon Cruanes	75e42072f4	wip: feat(leancheck): store intermediate objects of the proof	2025-01-27 21:52:00 -05:00
Simon Cruanes	39aa3d7f64	feat(level): more judgements	2025-01-27 21:51:59 -05:00
Simon Cruanes	2c435a5c18	fix(level): missing cases, inspiration from Trepplein	2025-01-27 21:51:59 -05:00
Simon Cruanes	cd07d6924b	details for leancheck	2025-01-27 21:51:59 -05:00
Simon Cruanes	70f0b3874c	wip: feat(leancheck): start binary to check lean proofs	2025-01-27 21:51:59 -05:00
Simon Cruanes	0b51dd172e	feat(level): implement level comparison	2025-01-27 21:51:59 -05:00
Simon Cruanes	1eeb5a464d	test: update test with levels	2025-01-27 21:51:59 -05:00
Simon Cruanes	9ea96a6b61	refactor: adapt to new levels in core	2025-01-27 21:51:59 -05:00
Simon Cruanes	b8cbe0cf06	feat(core-logic): add level expressions, modify type checker	2025-01-27 21:51:59 -05:00
Simon Cruanes	4363fc47b6	update smtlib	2025-01-27 21:51:51 -05:00
Simon Cruanes	6c8d6840f8	chore: update workflows	2025-01-27 21:49:09 -05:00
Simon Cruanes	90a5c7bc06	ocamlforamt	2025-01-27 21:49:05 -05:00
Simon Cruanes	8e6036bf3f	chore: CI	2023-12-27 19:45:57 -05:00
Simon Cruanes	13440d60f6	chore: CI	2023-12-27 19:31:55 -05:00
Simon Cruanes	eff6016151	support trace-fuchsia if present	2023-12-27 17:24:35 -05:00
Simon Cruanes	54077446ca	require ocaml 4.08, compat with containers 3.13	2023-12-07 00:14:16 -05:00
Simon Cruanes	85c39d3642	faster CI	2023-12-07 00:03:36 -05:00
Simon Cruanes	43c8e60790	use trace instead of our own custom tracing setup	2023-10-06 22:04:15 -04:00
Simon Cruanes	4bb15f8b5e	comments	2023-10-06 21:35:23 -04:00
Simon Cruanes	c35d721c6d	fix: compute model even if (potentially) new interface eqns are produced ... close #19	2023-06-28 11:42:26 -04:00
Simon Cruanes	3ebc532486	more tests	2023-06-26 15:40:38 -04:00
Simon Cruanes	923cbec6e5	remove debug msg	2023-06-26 15:40:38 -04:00
Simon Cruanes	8d8ef4211b	fix sign error	2023-06-26 15:40:38 -04:00
Simon Cruanes	67e9eabf43	add another bug repro	2023-06-26 15:40:38 -04:00
Simon Cruanes	477c780f18	CI	2023-06-26 15:40:38 -04:00
Simon Cruanes	d8612f84c9	doc	2023-06-26 15:40:38 -04:00
Simon Cruanes	2e29ab20dd	fix benchpress config	2023-06-26 15:40:38 -04:00
Simon Cruanes	3ba2583966	fix lra: define expressions occurring in subterms properly ... these sub-expressions need to be registered in the Simplex, possibly using an intermediate variable in case there's an offset.	2023-06-26 15:40:38 -04:00
Simon Cruanes	c4d3c44c49	warnings and comments	2023-06-26 15:40:38 -04:00
Simon Cruanes	c64bebaf6f	fix warning	2023-06-26 15:40:38 -04:00
Simon Cruanes	dcdc55ee1f	add non reduced test too	2023-06-26 15:40:38 -04:00
Simon Cruanes	87f9be7fe0	test: add regression test for LRA bug	2023-06-26 15:40:38 -04:00
Simon Cruanes	619da6fbcb	fix warnings	2023-06-23 20:44:01 -04:00
Simon Cruanes	7fbfb8439b	Merge branch 'master' into wip-produce-smtlib-models	2023-04-20 22:10:03 -04:00
Simon Cruanes	659f69f989	opam	2023-04-20 10:40:44 -04:00
Simon Cruanes	40a743badb	update to handle mtime 2.0	2023-02-23 21:02:21 -05:00
Simon Cruanes	4c330e4ed6	ocamlformat	2023-02-23 21:01:34 -05:00
Simon Cruanes	f5ccbb476b	add todo	2022-10-23 20:58:25 -04:00
Simon Cruanes	651f2c1150	warnings	2022-10-23 20:56:10 -04:00
Simon Cruanes	7f5c6d4131	wip: check models	2022-10-23 20:56:05 -04:00