I ended up enabling an additional UART. The docs say e.g. "UART3 GPIOs 4 - 7". I assumed this meant TX was on GPIO4 and RX was on GPIO7. Eventually I figured out that it actually meant that TX,RX,CTX,RTS were on GPIOs 4,5,6,7. I suppose in retrospect it's obvious, but it would be helpful if the wiki was a little more explicit. However, this isn't a completely satisfactory workaround, because some GPS hardware explicitly designed for the Raspberry Pi doesn't allow changing what TX/RX pins are used (notably this one
https://store.timebeat.app/products/gnss-raspberry-pi-cm4-module?variant=42280855699627).
This in the wiki is incorrect
The new devices will appear as /dev/ttyAMA0-4. Note that the numbering is simply counting through the activated devices. The numbers are not linked to any UART specifically. Only activating UART0 and UART5 will make UART5 be available as /dev/ttyAMA1.
If I enable just uart3, I get /dev/ttyAMA3.
I found the Serial devices section of the wiki confusing, particularly the description of UART 0/1
Raspberry Pis up to but not including the 4-series have only one UART which is UART0/1 (depending on which chip you use).
It mentions
dtoverlay=pi3-disable-bt
But I think the right one to use currently is simply
dtoverlay=disable-bt
This makes /dev/ttyAMA0 (a PL011) be connected to the TX/RX pins. Without this it's /dev/ttyS0 that's connected to the TX/RX pins (and there's a /dev/ttyAMA1).
James