Commit graph

18 commits

Author SHA1 Message Date
tydeu
185e10f6f3 misc: hoist facet name check to load + related bugfixes/refactors 2022-07-07 21:38:55 -04:00
tydeu
44f8e27a29 refactor: LeanExe.facet -> exeFacet 2022-07-05 17:46:44 -04:00
tydeu
0875473b13 fix: parameterize CustomData by package and target name 2022-07-04 20:27:10 -04:00
tydeu
7049a8da5f refactor: DynamicType -> FamilyDef
Uses more principled terminology (i.e., its really an open type family)
2022-07-04 17:21:36 -04:00
tydeu
906bc3c9c2 refactor: simplify custom target API (for now) 2022-07-01 16:26:35 -04:00
tydeu
2f9eefd35a feat: inductive BuildKey + proper custom targets 2022-07-01 04:52:50 -04:00
tydeu
72f555dd5b fix: properly trace module imports 2022-07-01 02:45:24 -04:00
tydeu
48d595b722 feat: preliminary custom package facets 2022-07-01 00:11:53 -04:00
tydeu
2ccd41ac82 feat: preliminary custom targets 2022-07-01 00:11:44 -04:00
tydeu
85f6d1a402 feat: preliminary custom module facets 2022-06-28 23:39:47 -04:00
tydeu
a4174a560b refactor: build code cleanup / reorg 2022-06-28 01:01:13 -04:00
tydeu
0e99494611 refactor: move lib/exe targets into the index 2022-06-27 02:07:45 -04:00
tydeu
c0bc0344b0 refactor: add LeanLib/LeanExe/ExternLib + reorg & cleanup 2022-06-26 18:26:12 -04:00
tydeu
3200b43371 feat: include external libraries in precompilation 2022-06-25 00:35:29 -04:00
tydeu
45ff2dbc9d feat: add isLeanOnly package config
closes leanprover/lake#74
2022-06-24 18:35:14 -04:00
tydeu
961a328bfd fix: report precompiled dynlibs to server
a feature of leanprover/lake#47 I had hetherto missed
2022-06-24 17:04:42 -04:00
tydeu
4f739572c9 refactor: use IndexT at Index.lean 2022-06-24 15:05:41 -04:00
tydeu
d842158172 refactor: reorg build code into smaller, focused files 2022-06-23 21:27:57 -04:00