Skip to content

Ambiguous-file-name warning

I was porting files related to abstract RTA and at some point I created file task.v in directory model/preemption/.
So I've got a situation when I have two files with name task -- model/task.v and model/preemption/task.v.

Now, when I try to import model/task.v via

From rt.restructuring.model Require Import task

I see the following warning. Moreover, as you can see, Coq loads file model/preemption/task.v instead of model/task.v.

Warning: task.vo has been found in
[ ./rt-proofs/restructuring/model/preemption ;
  ./rt-proofs/restructuring/model ];
loading ./rt-proofs/restructuring/model/preemption/task.vo
[ambiguous-file-name,filesystem]

One solution I see is replacing From rt.restructuring.model Require Import task with From rt.restructuring Require Import model.task.
But is it possible to fix this problem in a more solid way (e.g. make imports more "conservative")?

@bbb @mlesourd @proux

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information