lean4 feat: lake: alternative TOML config

Work-in-progress PR for an alternative TOML configuration file for basic packages.

Task list

[x] TOML parser
[x] TOML data types
[x] TOML elaborator (Syntax -> data types)
[x] TOML tests
[ ] Lake configuration from TOML
[x] lakefile.toml loader
[ ] lake translate <toml|lean> to switch between config languages
[ ] TOML option for Lake package templates (e.g., lake init <pkg> --toml)

Feb 10 '24 00:02 tydeu

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-3298 build against this PR was cancelled. (2024-02-10 01:32:15) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-02-10 02:45:15) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-02-10 03:22:16) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-02-12 17:49:23) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-02-14 02:13:43) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-04 22:37:25) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-06 21:17:55) View Log
🟡 Mathlib branch lean-pr-testing-3298 build this PR didn't complete normally. (2024-03-07 00:07:54) View Log
🟡 Mathlib branch lean-pr-testing-3298 build this PR didn't complete normally. (2024-03-13 23:49:10) View Log
🟡 Mathlib branch lean-pr-testing-3298 build this PR didn't complete normally. (2024-03-14 01:16:38) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-14 16:44:23) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-18 18:14:18) View Log
🟡 Mathlib branch lean-pr-testing-3298 build against this PR was cancelled. (2024-03-18 22:53:25) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-19 00:05:58) View Log
🟡 Mathlib branch lean-pr-testing-3298 build against this PR was cancelled. (2024-03-19 22:31:43) View Log
🟡 Mathlib branch lean-pr-testing-3298 build against this PR was cancelled. (2024-03-19 23:38:06) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-20 00:52:40) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-20 23:49:44) View Log
🟡 Mathlib branch lean-pr-testing-3298 build against this PR was cancelled. (2024-03-26 00:11:03) View Log
🟡 Mathlib branch lean-pr-testing-3298 build against this PR was cancelled. (2024-03-26 00:42:19) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-26 01:53:22) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-26 20:50:51) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-27 04:39:37) View Log
🟡 Mathlib branch lean-pr-testing-3298 build against this PR was cancelled. (2024-03-27 17:33:34) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-27 18:44:42) View Log
✅ Mathlib branch lean-pr-testing-3298 has successfully built against this PR. (2024-03-28 03:49:00) View Log

Feb 10 '24 01:02 leanprover-community-mathlib4-bot

Sounds great. Looking forward to seeing this in a nightly so we can start translating ahead of v4.8.

Mar 26 '24 05:03 kim-em