PLFA 2025 10 27: change how eval is defined

[wadler]

Following a suggestion of Conrad Watt, changed the definition of eval to add information. Recall that the evaluator takes an amount of gas and a term and returns a reduction sequence. If the evaluator runs out of gas it returns a sequence of length equal to the amount of gas, while if it terminates in returns a sequence of length less than the amount of gas and ending in a value.

[wadler]

I see there are some issues above but I'm not sure what's causing them. @wenkokke, can you please sort it out, or if not let me know what I should do?

[wadler]

@wenkokke I can see that all of the checks are failing with various issues, but they seem unrelated to the code changed in the pull request. What is the next step?

[wadler]

@wenkokke I can see there is an option to "update branch" to merge in more recent changes from dev, which you've already done once. I guess there are now more recent changes. Can you merge them again? Will that fix the issues?

[wenkokke]

@wenkokke I can see that all of the checks are failing with various issues, but they seem unrelated to the code changed in the pull request. What is the next step?

Given that those same checks succeed on HEAD, I would assume it's something that is related to the changes in this PR, but I might be wrong.

[wadler]

Hey, @wenkokke this pull request has been stuck for months now. Any suggestions on what I should do to get it unstuck?

[wenkokke]

@wadler This appears to be a bug in the HTML parser that I'm using where the use of <g and x<s as variable names trips it up somehow. I've undone one of your rewrites, which mentions the evidence in the explanation of the proof, which seems to unbreak the PR.