41 commits

Author	SHA1	Message	Date
tydeu	ca04bf9b43	refactor: reorg cli code some (e.g., split cmds into defs)	2022-07-08 22:51:07 -04:00
tydeu	185e10f6f3	misc: hoist facet name check to load + related bugfixes/refactors	2022-07-07 21:38:55 -04:00
tydeu	8c46d7439a	chore: remove some deprecated features + deprecate extraDepTarget	2022-07-01 15:35:45 -04:00
tydeu	a81994871a	feat: add build types (e.g., debug, release)	2022-07-01 14:45:19 -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	62815168c6	feat: library-level module configuration	2022-06-26 20:35:23 -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	d3c373478e	refactor: generalize module facet build code to any target	2022-06-23 13:19:39 -04:00
tydeu	f7451e025c	feat: basic precompiled modules + builtin module facets ... closes leanprover/lake#47	2022-06-22 13:20:15 -04:00
Leonardo de Moura	8d854900fd	chore: replace constant with opaque	2022-06-16 17:33:00 -04:00
tydeu	02ee011a0e	refactor: simplify module target code + related cleanup ... closes leanprover/lake#75	2022-06-16 02:04:31 -04:00
tydeu	7ea84c5961	doc: update defaultFacet description	2022-06-10 16:13:55 -04:00
tydeu	144fbaf642	doc: update w/ extern_lib + some cleanup	2022-06-10 15:16:49 -04:00
tydeu	e5782adeff	feat: replace moreLibTargets w/ new extern_lib syntax	2022-06-10 12:08:58 -04:00
tydeu	5fdf97db20	feat: none package facet to avoid warnings in scripts example	2022-06-09 19:12:29 -04:00
tydeu	964eb5ef10	doc: update with new features + other cleanup	2022-06-09 18:58:43 -04:00
tydeu	108d9852ca	chore: deprecate package facets	2022-06-09 16:38:07 -04:00
tydeu	9dadf7e0b1	feat: attr to mark targets as package defaults	2022-06-09 12:52:54 -04:00
tydeu	9c20cad9d8	feat: syntax for defining extra lib & exe targets	2022-06-08 17:06:03 -04:00
tydeu	18eef56322	feat: multi lib & exe targets w/ updated build CLI syntax	2022-06-07 20:48:41 -04:00
tydeu	b6bce412a9	refactor: split lib and exe config from package	2022-06-07 16:48:55 -04:00
tydeu	c19417b86a	feat: new require syntax for package deps	2022-06-01 16:26:39 -04:00
tydeu	85e3385aaa	feat: only update deps in configure + don't ignore manifest.json ... closes leanprover/lake#59, leanprover/lake#63	2022-05-23 20:38:54 -04:00
Gabriel Ebner	712b22b46f	perf: do not import Lean.Elab.Frontend from Lake	2022-05-15 15:56:50 -04:00
tydeu	30e3f10c6c	chore: ilean code cleanup	2022-01-31 00:04:17 -05:00
Leonardo de Moura	e880dd52a4	chore: PointedType	2022-01-14 20:41:47 -08:00
tydeu	1b96c466ca	refactor: use new version info from Lean + cleanup	2021-12-19 21:59:17 -05:00
tydeu	8fb9dd8478	fix: consider globbed files local ... easiest way to fix mathport builds (for now)	2021-12-16 21:56:10 -05:00
tydeu	8e728b1159	refactor: split Package and Workspace	2021-12-04 12:58:00 -05:00
tydeu	fcc3e3d93e	chore: cleanup	2021-12-02 21:29:16 -05:00
tydeu	a7a980c12d	refactor: remove unused branch parameter from Source.git	2021-12-02 21:25:53 -05:00
tydeu	a1368df5c9	chore: fix docstring formatting	2021-11-26 23:47:36 -05:00
tydeu	40b6ca82b3	fix: include libleanshared in Lean trace ... closes leanprover/lake#26	2021-11-11 02:23:54 -05:00
tydeu	36b0d7b60c	feat: store current Package in BuildM	2021-11-11 00:10:52 -05:00
tydeu	8d96c2cbe8	refactor: move Workspace/Script code to separate files	2021-11-10 18:46:31 -05:00
tydeu	331bf0f7f2	refactor: reorganize code folder structure	2021-11-09 22:55:21 -05:00

Renamed from Lake/Package.lean (Browse further)