Add additional digits to gauge IDs

[mandli]

As discussed on claw-users if you have too many gauges such that you have more than $10^5$ gauges GeoClaw will not warn the user and will simply loop around, corrupting the output files. It was also pointed out that it would be convenient to be able to directly use the gauge IDs that are often greater than 5 digits and for coastal stations are 7 digits long.

I would propose:

1. that we increase the digits to at least 7 if not 8 so that we have a little wiggle room and 8 digits seems nice and
2. add code that would warn someone if they did go over the now $10^8$ cap (although unlikely).

[rjleveque]

It would be good to add a warning in general. I doubt anyone will have more than 1e7 gauges, but it's quite possible someone will try to use a gauge number with more than 8 digits in order to match a numbering system used by some other agency. (NOAA generally uses 7 digit gauge numbers).

[mandli]

Good point on the simple overflow. This could probably be implemented in Python quite easily now that I think about it.

[mandli]

I was thinking about this again and wanted to ping those interested as to how we change the name. Options I came up with:

1. Keep the file format but just add more digits, gauge00123456.txt
2. Only keep the non-zero left digits, gauge123456.txt
3. Keep the field width the same but add an underscore for readability, gauge_00123456.txt

The last of these could also do the only non-zero left digits too.

[rjleveque]

Having leading zeros is useful if you have e.g. gauge numbers 1 to 100 and you want ls or other sorting tools to list them in order, but that's not a big deal.

One other possibility would be to have e.g. 7 digits with leading zeros by default, but with the option that more than 7 digits can also be handled, e.g. in Python:

>>> fname = lambda gaugeno: 'gauge%s.txt' % str(gaugeno).zfill(7)

>>> fname(1234)
'gauge0001234.txt'

>>> fname(123456789)
'gauge123456789.txt'

Or even make the default 5 digits with leading zeros to agree with the current naming scheme but allow more digits. (I think I prefer this for backward compatibility and because 7 digits seems more unwieldy in general, and often not needed.)

I don't really think we need an underscore, but don't feel strongly about that.

[mandli]

I like the suggestion to always have at least 5 digits but allow more if requested.

The _ I was not entirely sure about an am fine dropping that idea.

[rjleveque]

Resolved in $615.