Stream: Coq users

Topic: Script to fix Instance locality warnings


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 15:57):

ah, but you mean the error below

view this post on Zulip Ralf Jung (Nov 24 2021 at 15:58):

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

view this post on Zulip Ralf Jung (Nov 24 2021 at 15:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 15:59):

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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:00):

interesting

view this post on Zulip 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

view this post on Zulip Ralf Jung (Nov 24 2021 at 16:01):

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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:01):

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

view this post on Zulip 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^^)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:03):

you should try the same

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:03):

I don't remember what the hardcoded paths were about

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:04):

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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:05):

did this work?

view this post on Zulip 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:

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:05):

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

view this post on Zulip Yannick Forster (Nov 24 2021 at 16:06):

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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:06):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:06):

you know, scripting

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:08):

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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2021 at 16:09):

ah

view this post on Zulip Ralf Jung (Nov 24 2021 at 16:09):

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

view this post on Zulip Ralf Jung (Nov 24 2021 at 16:09):

thanks!

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC