feat: Allow selective continuation of goals #27

Merged
aniva merged 14 commits from goal/continuation into dev 2023-11-07 16:49:56 -08:00
Owner
  1. Goal continuation now can selectively continue goals
  2. Continuation fails when the target state has unresolved goals (helps with bugs during reconstruction)
  3. goal.continue command added.
  4. Print the name of the root metavariable in goal.start (for consistency in bookkeeping)
1. Goal continuation now can selectively continue goals 2. Continuation fails when the target state has unresolved goals (helps with bugs during reconstruction) 3. `goal.continue` command added. 4. Print the name of the root metavariable in `goal.start` (for consistency in bookkeeping)
aniva added the
part/Goal
category
feature
labels 2023-11-03 23:43:43 -07:00
aniva self-assigned this 2023-11-03 23:43:43 -07:00
aniva added this to the 0.2.8 milestone 2023-11-03 23:44:38 -07:00
aniva added 5 commits 2023-11-04 15:54:42 -07:00
aniva added 1 commit 2023-11-06 10:45:41 -08:00
dbace9f2d5
fix: Use Lean's built in name parser
The `str_to_name` parser cannot handle numerical names and escapes.
aniva added 1 commit 2023-11-06 11:04:43 -08:00
aniva added 1 commit 2023-11-06 11:45:58 -08:00
aniva added 1 commit 2023-11-06 11:51:45 -08:00
aniva added 1 commit 2023-11-06 12:20:19 -08:00
aniva added 1 commit 2023-11-07 12:10:16 -08:00
aniva added 1 commit 2023-11-07 12:11:23 -08:00
aniva added 1 commit 2023-11-07 13:08:15 -08:00
aniva added 1 commit 2023-11-07 13:10:28 -08:00
Author
Owner

Tested on aniva/Trillium#69 and seems stable. Merge.

Tested on https://git.leni.sh/aniva/Trillium/pulls/69 and seems stable. Merge.
aniva merged commit c99125c4a6 into dev 2023-11-07 16:49:56 -08:00
aniva deleted branch goal/continuation 2023-11-07 16:49:56 -08:00
Sign in to join this conversation.
No description provided.