Zulip Chat Archive

Stream: mathlib4

Topic: fatal: ambiguous argument 'mathlib4#771..HEAD'


Kevin Buzzard (Nov 28 2022 at 22:14):

Is this happening for other people too:

~/lean-projects/mathlib$ ./scripts/port_status.py
fatal: ambiguous argument 'mathlib4#771..HEAD': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
fatal: ambiguous argument 'mathlib4#763..HEAD': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
fatal: ambiguous argument 'mathlib4#762..HEAD': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
# The following files have all dependencies ported already, and should be ready to port:
# Earlier items in the list are required in more places in mathlib.
control.traversable.basic
algebra.hom.group    -- mathlib4#659 8c53048add6ffacdda0b36c4917bfe37e209b0ba
data.nat.basic    -- WIP mathlib4#729 71ca477041bcd6d7c745fe555dc49735c12944b7
control.applicative

[seems to work fine after the errors...]

Scott Morrison (Nov 28 2022 at 22:20):

Yes, it's malformed entries in the port-status wiki page. If you search for mathlib4#771 you'll find it still says "PR" in that line. (Or it did, until I fixed some a moment ago.)

Eric Wieser (Nov 28 2022 at 22:39):

I think if we merge #17620 we would end up with better behavior here when the file is malformed

Scott Morrison (Nov 28 2022 at 22:58):

Yes, lets. @Patrick Massot, could you do a release of mathlib-tools?

Patrick Massot (Nov 29 2022 at 07:58):

I released.


Last updated: Dec 20 2023 at 11:08 UTC