Script to fix Instance locality warnings · Coq users

Stream: Coq users

Topic: Script to fix Instance locality warnings

Ralf Jung (Nov 24 2021 at 15:52):

@Pierre-Marie Pédrot I am trying to use your script to fix the Instance locality warnings. So I am feeding it the part of https://gitlab.mpi-sws.org/iris/simuliris/-/jobs/159456 with the Coq output, but I get

$ ~/src/coq/instance-hint-adapt.ml warn
File "/home/r/src/coq/instance-hint-adapt.ml", line 64, characters 24-42:
64 |   let todo = List.sort (Pervasives.compare : int -> int -> int) todo in
                             ^^^^^^^^^^^^^^^^^^
Alert deprecated: module Stdlib.Pervasives
Use Stdlib instead.

If you need to stay compatible with OCaml < 4.07, you can use the
stdlib-shims library: https://github.com/ocaml/stdlib-shims
Exception: Sys_error "behavior.v: No such file or directory".

Any idea what might be happening here? My working dir is the root of the simuliris repo, same as for the build log.

Pierre-Marie Pédrot (Nov 24 2021 at 15:56):

You're using a version of OCaml that's too modern, as hinted by the warning replace the Pervasive module by Stdlib in the source

Pierre-Marie Pédrot (Nov 24 2021 at 15:57):

ah, but you mean the error below

Ralf Jung (Nov 24 2021 at 15:58):

yeah I guess the deprecation warning doesnt matter (but I dont know)

Ralf Jung (Nov 24 2021 at 15:58):

also quite funny that for once something in Debian is "too modern" :D

Pierre-Marie Pédrot (Nov 24 2021 at 15:58):

the script must be tweaked to have the file in path, i.e. if the warnings mention "behavior.v" you must be in the right pwd

Pierre-Marie Pédrot (Nov 24 2021 at 15:59):

well Coq is arguably stuck to 4.07 for good or bad reasons so that's what I use daily

Ralf Jung (Nov 24 2021 at 15:59):

this repo has 6-10 directories, I cant be in the pwd for all of them... so not quite sure what you mean?

Pierre-Marie Pédrot (Nov 24 2021 at 15:59):

look at the warning file, it probably mentions behavior.v

Pierre-Marie Pédrot (Nov 24 2021 at 16:00):

the script looks for behavior.v, doesn't find it because it's inside a subfolder, and dies

Ralf Jung (Nov 24 2021 at 16:00):

not really

$ grep behavior.v warn
COQC theories/simulation/behavior.v
COQC theories/stacked_borrows/behavior.v
COQC theories/simulang/behavior.v
File "./theories/simulang/behavior.v", line 39, characters 0-4:
File "./theories/simulang/behavior.v", line 46, characters 0-4:

Pierre-Marie Pédrot (Nov 24 2021 at 16:00):

interesting

Pierre-Marie Pédrot (Nov 24 2021 at 16:00):

tweak it so that it doesn't chop off the head of the file name

Ralf Jung (Nov 24 2021 at 16:01):

you can basically assume that I dont know OCaml...^^

Pierre-Marie Pédrot (Nov 24 2021 at 16:01):

honestly this is really a hacky script I wrote in 5 minutes to get the job done

Pierre-Marie Pédrot (Nov 24 2021 at 16:01):

c'mon, how can you write Coq and don't speak the ML dialect?

Ralf Jung (Nov 24 2021 at 16:01):

right but it also seems like the best option we have. though I guess alternatively I can wait until @Gaëtan Gilbert 's PR lands and then use Tej's script (which he wrote in 5min to get the job done^^)

Pierre-Marie Pédrot (Nov 24 2021 at 16:03):

@Yannick Forster mentioned that removing the let f = String.sub f 20 (String.length f - 20) in was enough for him

Pierre-Marie Pédrot (Nov 24 2021 at 16:03):

you should try the same

Pierre-Marie Pédrot (Nov 24 2021 at 16:03):

I don't remember what the hardcoded paths were about

Pierre-Marie Pédrot (Nov 24 2021 at 16:04):

if this works I'll push the fixed version to the repo

Ralf Jung (Nov 24 2021 at 16:04):

Pierre-Marie Pédrot said:

c'mon, how can you write Coq and don't speak the ML dialect?

this looks pretty different from Gallina, I do honestly have a hard time even reading that code

Pierre-Marie Pédrot (Nov 24 2021 at 16:05):

did this work?

Ralf Jung (Nov 24 2021 at 16:05):

Pierre-Marie Pédrot said:

Yannick Forster mentioned that removing the let f = String.sub f 20 (String.length f - 20) in was enough for him

okay that helps. :)
still some problems though:

it adds the Global on a new line, instead of adding it at the beginning of the existing line
it sometimes adds two Global (but not too often so I guess I can fix it by hand)

Pierre-Marie Pédrot (Nov 24 2021 at 16:05):

yeah the two global stuff is because it's really a heuristic

Yannick Forster (Nov 24 2021 at 16:06):

I also experienced both. Didn't care about the first, fixed the second manually

Pierre-Marie Pédrot (Nov 24 2021 at 16:06):

it looks for lines up to 20 lines above to find something that looks like an instance

Pierre-Marie Pédrot (Nov 24 2021 at 16:06):

you can tweak the max_diff value if you want to look further

Pierre-Marie Pédrot (Nov 24 2021 at 16:06):

you know, scripting

Pierre-Marie Pédrot (Nov 24 2021 at 16:07):

if you want to fix the first point just add a \n character line 56

Ralf Jung (Nov 24 2021 at 16:08):

I dont understand how that heuristic leads to double-global -- it stops that search when it finds something, right? so each warning adds no more than 1 Global?

Pierre-Marie Pédrot (Nov 24 2021 at 16:08):

(hm, maybe it'll wreak havoc w.r.t. line numbering)

Ralf Jung (Nov 24 2021 at 16:08):

Pierre-Marie Pédrot said:

if you want to fix the first point just add a \n character line 56

I want it to add fewer newlines, not more

Pierre-Marie Pédrot (Nov 24 2021 at 16:09):

Ralf Jung (Nov 24 2021 at 16:09):

but its okay, I can probably get sed to do that

Ralf Jung (Nov 24 2021 at 16:09):

thanks!

Pierre-Marie Pédrot (Nov 24 2021 at 16:09):

then concat the string to x and turn off + 1 into off below

Last updated: Sep 26 2023 at 11:01 UTC