New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Stabler gensym #1555

Open
mtzguido opened this Issue Oct 8, 2018 · 0 comments

Comments

Projects
None yet
1 participant
@mtzguido
Contributor

mtzguido commented Oct 8, 2018

This is very low prio, but it usually happens that when touching Prims or some other file high in the dependency graph, we get spurious diffs in many other files. Since we check-in the snapshot, and we need to have it up-to-date, we get very verbose commits when nothing relevant changed. Plus, when something did change, it's hard to spot.

Example: I removed a few lines in prims and get things like this:

diff --git a/src/ocaml-output/FStar_Common.ml b/src/ocaml-output/FStar_Common.ml
index 64fcd1d336..1d7ce6e583 100644
--- a/src/ocaml-output/FStar_Common.ml
+++ b/src/ocaml-output/FStar_Common.ml
@@ -1,7 +1,7 @@
 open Prims
 let (has_cygpath : Prims.bool) =
   try
-    (fun uu___67_3  ->
+    (fun uu___67_5  ->
        match () with
        | () ->
            let t_out =
@@ -9,23 +9,23 @@ let (has_cygpath : Prims.bool) =
                FStar_Pervasives_Native.None
               in
            (FStar_Util.trim_string t_out) = "/usr/bin/cygpath") ()
-  with | uu___66_6 -> false 
+  with | uu___66_18 -> false 
 let (try_convert_file_name_to_mixed : Prims.string -> Prims.string) =
   let cache = FStar_Util.smap_create (Prims.parse_int "20")  in
   fun s  ->
     if has_cygpath && (FStar_Util.starts_with s "/")
     then
-      let uu____15 = FStar_Util.smap_try_find cache s  in
-      match uu____15 with
+      let uu____39 = FStar_Util.smap_try_find cache s  in
+      match uu____39 with
       | FStar_Pervasives_Native.Some s1 -> s1
       | FStar_Pervasives_Native.None  ->
           let label = "try_convert_file_name_to_mixed"  in
           let out =
-            let uu____21 =
+            let uu____54 =
               FStar_Util.run_process label "cygpath" ["-m"; s]
                 FStar_Pervasives_Native.None
                in
-            FStar_All.pipe_right uu____21 FStar_Util.trim_string  in
+            FStar_All.pipe_right uu____54 FStar_Util.trim_string  in
           (FStar_Util.smap_add cache s out; out)
     else s
...

Possibly related to #1484, which I think is caused by cached files (not) affecting the gensym state.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment