Two flags for printing goals: -upto and -lastgoals

[namasikanam]

Two flags for printing goals.

• -upto compiles up to a position and prints goals there
• -lastgoals prints the last unproven goals

I add these two flags for MCP, so that the coding agent can see the goals as needed.

[fdupress]

Extend and use LSP instead.

[strub]

Reopening (I changed my mind). I will review it. I don't think these are the exact options that we want and this will allow LLM to have a rough interface to EasyCrypt when the (to come) MCP is not in used.

[strub]

@namasikanam Can you explain what instructions you give to an LLM to use these options? Maybe you could document?

[namasikanam]

@strub These are the instructions I gave. They simply explain the option and the tactic.

* The command for easycrypt is `easycrypt compile -no-eco -lastgoals -script blabla.ec`, where the option `-lastgoals` are for printing the last unproven goals when printing.
* You can use `-upto LINE` or `-upto LINE:COL` to compile up to a position and print proof goals there. If the compilation fails, the last unproven goals should be printed.

I can document them. I think they are already documented in the help message. If they need better documenting, do you think where is the best place? Maybe the main readme?

For an MCP of EC, I think it's better to have two modes. 1. compilation mode, which are on the top of easycrypt compile with some options, where coding agent can edit files and compile and see where it gets stuck. 2. interaction mode, which is based on LSP, where coding agent can derive proofs step by step.

My design of the usage of these two modes follows how human deals with EC proofs. The compilation mode is used globally to check whether a file is finished or quickly jump to the sticking point, while the interaction mode is used locally to figure out how to close a proof.