You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The general problem with .v and .glob files having the same time is that we can't tell whether the .v file has been updated since the .glob file was generated. Fixing this requires threading through information about which files are expected to fail coqc compilation (the buggy ones only), which files must have up to date .globs even if compilation fails (the ones that the minimizer modifies), and which files we should perhaps not attempt to update the .globs on (ones in user-contrib, for example, or anything that was taken from COQPATH)
The text was updated successfully, but these errors were encountered:
The general problem with .v and .glob files having the same time is that we can't tell whether the .v file has been updated since the .glob file was generated. Fixing this requires threading through information about which files are expected to fail coqc compilation (the buggy ones only), which files must have up to date .globs even if compilation fails (the ones that the minimizer modifies), and which files we should perhaps not attempt to update the .globs on (ones in user-contrib, for example, or anything that was taken from COQPATH)
The text was updated successfully, but these errors were encountered: