Minification will remove an import that is transitively depended on

[Durbatuluk1701]

_CoqProject:

-R . Test
Test1.v
Test2.v
Test3.v

Test1.v:

Definition thing (x: nat) : nat :=
  x.

Test2.v:

Require Import Test1.

Test3.v:

Require Import Test2.

Lemma uses_thing : forall x,
  Test1.thing x = x.
Proof.
  reflexivity.
Qed.

Running coq-tools/minimize-requires.py --all -f _CoqProject will modify Test2.v by removing the Require Import Test1. However this will cause the project to no longer build as Test1.thing is no longer available in the environment.

[JasonGross]

Indeed, this is a defect that results from wanting to avoid recompiling the entire project on every change to every file. However, we should probably add a flag --keep-transitive-dependencies (or similar) that runs the expensive check. (PRs welcome!)

[Durbatuluk1701]

What would your thoughts be on a possible alternate approach where we basically have two phases of minification:

1. Directly import all transitively depended upon files
2. Work forward (i.e. in CoqProject order) with the binary search to reduce the number of imports.

If I am thinking about it correctly we would not have any need to backtrack and would still end up with a minimal number of imports.
The downside would likely be that later files would likely have a much larger search to perform, although hopefully the binary search would help with that.

[JasonGross]

Yes, this should work. For 1, there is already code in the bug minimizer that adds all transitive Requires to the top of the file. Probably we want a slightly different variant that doesn't split apart later Require Imports, and if we want to be extra robust, we may want to try inserting transitive Requires right before each existing Require rather than all at the top of the file.

Regarding 2, I don't think binary search helps much. We can perhaps do binary search on the transitive Requires of each original Requirement, but in general we're searching a space of size 2ⁿ (since each Require can be present or not) and so cannot uniformly do much better then linear traversal of the Requires. (If we have reason to believe that we'll be removing some subset more often than not, e.g., as in the case of the transitive Requires of each original Require, then we may do better by trying a couple steps of binary search locally.)

---

Note, however, that Step 1 is not 100% safe because global side effects of Require are order-dependent, so we may still want the quadratic time version.

[JasonGross]

Some incomplete notes if you (or anyone else) wants to implement this: I believe the first steps are:

1. Add a --add-transitive-requires-before-minimizing flag to gate this behavior
2. Add a first_strip_requires=False argument to disable the strip_requires in

   coq-tools/coq_tools/replace_imports.py

   Lines 148 to 163 in d74f07b

   	def normalize_requires(filename, **kwargs):
   	"""Return the contents of filename, with all [Require]s split out and ordered at the top.
   	Preserve any leading whitespace/comments.
   	"""
   	if filename[-2:] != '.v': filename += '.v'
   	kwargs = fill_kwargs(kwargs)
   	lib = lib_of_filename(filename, **kwargs)
   	all_imports = run_recursively_get_imports(lib, **kwargs)
   	v_name = filename_of_lib(lib, ext='.v', **kwargs)
   	contents = get_file(v_name, **kwargs)
   	header, contents = split_leading_comments_and_whitespace(contents)
   	contents = strip_requires(contents)
   	contents = ''.join('Require %s.\n' % i for i in all_imports[:-1]) + '\n' + contents.strip() + '\n'
   	return header + contents

   (note we can already pass absolutize=() to bypass the get_file normalization logic)
3. (Optional) Add a variant of

   coq-tools/coq_tools/import_util.py

   Line 1277 in d74f07b

   def run_recursively_get_imports(

   that includes require locations, so we can add transitive dependencies right before each require if we want to
4. Join requires when --add-transitive-requires-before-minimizing is passed as in

   coq-tools/coq_tools/find_bug.py

   Lines 1004 to 1016 in d74f07b

   	def try_normalize_requires(output_file_name, **kwargs):
   	contents = read_from_file(output_file_name)
   	old_contents = contents
   	# we need to clear the libimport cache to get an accurate list of requires
   	clear_libimport_cache(lib_of_filename(output_file_name, **kwargs))
   	new_contents = normalize_requires(output_file_name, update_globs=True, **kwargs)
   	check_change_and_write_to_file(old_contents, new_contents, output_file_name,
   	unchanged_message='No Requires to normalize.',
   	success_message='Succeeded in normalizing Requires.',
   	failure_description='normalize Requires',
   	changed_descruption='Normalized Requires file',
   	**kwargs)