lean4-htt/tests/pkg
Mac Malone 34385b8ee8
feat: lake: use absolute paths (#7822)
This PR changes Lake to use normalized absolute paths for its various
files and directories.

This is done by storing absolute paths for the workspace directory,
package directories, and configuration files. These are then joined to
relative paths (e.g., for source directories) using a custom join
function that eliminates `.` paths.

Closes #7498. Closes #4042.
2025-04-05 13:38:35 +00:00
..
builtin_attr fix: make sure monad lift coercion elaborator has no side effects (#6024) 2024-11-13 16:22:31 +00:00
debug feat: debug_assert! (#7256) 2025-03-03 16:34:44 +00:00
deriving chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
frontend feat: lake: support plugins (#7001) 2025-02-14 04:57:31 +00:00
initialize fix: missing unboxing in interpreter when loading initialized value (#4512) 2024-06-20 10:06:24 +00:00
misc feat: allow duplicate theorems to be imported 2024-03-13 12:57:41 -07:00
path with spaces fix: calling programs with spaces on Windows (#4515) 2024-07-26 17:35:05 +00:00
prv feat: structure instance notation elaboration improvements (#7717) 2025-03-30 17:40:36 +00:00
test_extern feat: lake: use absolute paths (#7822) 2025-04-05 13:38:35 +00:00
user_attr chore: simp_arith has been deprecated (#7043) 2025-02-12 03:55:45 +00:00
user_attr_app feat: importModules without loading environment extensions (#6325) 2025-04-02 08:37:11 +00:00
user_ext chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
user_opt feat: accept user-defined options on the cmdline (#4741) 2024-08-02 12:24:56 +00:00
user_plugin feat: smarter plugin loading (#7090) 2025-02-18 23:03:52 +00:00
.gitignore chore: ignore forgotten Lake test artifacts 2023-11-17 21:25:41 -05:00