Skip to content

[Bug] [Lean] Save as exercise-sheet does not empty input areas #314

@pimotte

Description

@pimotte

What happened?

With a Lean exercise sheet, it should be possible "Save as exercise sheet"

How can we reproduce this issue?

Example:

  1. Open the Lean ATP file
  2. Execute the "Save as exercise sheet" command: Ctrl + Shift + P > Waterproof: Save as exercise sheet
  3. Open the saved file and notice that the input areas are not empty.

What was supposed to happen?

Save as exercise sheet should remove solutions to exercises by emptying input areas.

Implementation notes:

We want to take this opportunity to refactor some stuff as well.

Plan:

  • Update typescript implementation of this functionality to include Lean files
  • Make sure typescript implementation is callable in script form
  • Convert this Python script to a typescript script that uses the implementation used for the command.
  • Expose the compiled version of this typescript script to something that can be run with npx
  • Update the CI in this repo to use npx @waterproof/vscode something something to do the conversion, rather than the existing python script.

Metadata

Metadata

Assignees

Labels

bugSomething isn't working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions