Add goal printing flags (-upto, -lastgoals) and LLM agent guide

[namasikanam]

Add two new flags for the easycrypt CLI to support LLM coding agents:

• -upto <pos>: compile up to a given position and print goals there
• -lastgoals: print the last unproven goals

Also add a dedicated llm command mode and an LLM agent guide
(doc/llm/CLAUDE.md) documenting EasyCrypt tactics and workflow for
use with AI coding assistants.

[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.

[namasikanam]

It seems that the last four commits in the main branch may have been unintentionally reverted by the merged commit of this PR :)

Maybe we can revert this PR, and re-do a clean PR which does not touch other modifications?

[alleystoughton]

It seems that the last four commits in the main branch may have been unintentionally reverted by the merged commit of this PR :)

Maybe we can revert this PR, and re-do a clean PR which does not touch other modifications?

Just making sure @strub saw this.