unstable print glob order of variables

[alleystoughton]

I'm finding some unstable behavior of print glob involving cacheing, which involves running a module declaration in ProofGeneral, doing the print glob, going back in ProofGeneral to edit the module declaration, and repeating the print glob. The results are the same, whereas they should not be (as verified by a fresh module declaration with the same contents, followed by yet another print glob.

I'm running on macOS Sonoma, GNU Emacs 29.1, the current EasyCrypt from main, ProofGeneral proof-general-20211217.1753 (in ELPA).

(* start in ProofGeneral with stepping through : *)

module M = {
  var x : int
  var y : int
}.

print glob M.

(*
we get:

Globals [# = 0]:

Prog. variables [# = 2]:
  M.y : int
  M.x : int

note that the variables are listed in
reverse order

now go back in ProofGeneral to the definition of M
and reverse the order of the variables:

  var y : int
  var x : int

repeat the `print glob M`, and we get:

Globals [# = 0]:

Prog. variables [# = 2]:
  M.y : int
  M.x : int
*)

module N = {
  var y : int
  var x : int
}.

print glob N.

(*
Globals [# = 0]:

Prog. variables [# = 2]:
  N.x : int
  N.y : int

now we are getting the normal behavior,
where the variables are listed in reverse
order *)

[alleystoughton]

I reproduced this just using EasyCrypt from the shell:

$ easycrypt
>> Copyright (c) 2012 IMDEA Software Institute
>> Copyright (c) 2012 Inria
>> Copyright (c) 2017 Ecole Polytechnique
>> Copyright (c) EasyCrypt contributors (see AUTHORS)
>> Distributed under the terms of the MIT license
>> Standard Library (theories/**/*.ec): 
>>  Distributed under the terms of the MIT license
>> 
>> GIT hash: r2022.04-322-g791bfa7
[0|check]>
module M = { var x : int var y : int }.
[1|check]>
print glob M.
Globals [# = 0]:

Prog. variables [# = 2]:
  M.y : int
  M.x : int
[2|check]>
undo 1.
[1|check]>
undo 0.
[0|check]>
print M.
no such object in any category
[1|check]>
module M = { var y : int var x : int }.
[2|check]>
print glob M.
Globals [# = 0]:

Prog. variables [# = 2]:
  M.y : int
  M.x : int
[3|check]>
module N = { var y : int var x : int }.
[4|check]>
print glob N.
Globals [# = 0]:

Prog. variables [# = 2]:
  N.x : int
  N.y : int
[5|check]>

[fdupress]

Reproduced—using easycrypt shell—on WSL (don't ask; with ocaml 4.13.1) and Arch Linux (with ocaml 5.2.0).

Could this be related to our continuous and roughly-linear memory growth with undo/redo loops? Some of the caching does not get undone and keeps stacking into the environment even through undos?

[strub]

See #612. However, this one is going to be hard to fix without breaking external proofs.