Merge pull request #194 from nyx-space/43-allow-to-ignore-leap-second…

…s-after-a-given-date

Add support for LeapSecondsFile and UT1

.github/workflows/formal_verification.yml

@@ -37,7 +37,7 @@ jobs:
           # Remove `cdylib` from targets in Cargo.toml because it confuses Kani
           sed '17d' Cargo.toml > Cargo.toml.new
           mv Cargo.toml.new Cargo.toml
-          cargo kani | (cargo kani --visualize && exit 1) # Re-run for artifacts if it has failed.
+          cargo kani
 
       - name: Save formal verification artifacts
         uses: actions/upload-artifact@v3

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "hifitime"
-version = "3.7.0"
+version = "3.8.0"
 authors = ["Christopher Rabotin <[email protected]>"]
 description = "Ultra-precise date and time handling in Rust for scientific applications with leap second support"
 homepage = "https://nyxspace.com/"
@@ -10,7 +10,7 @@ keywords = ["date", "time", "science", "leap-second", "no-std"]
 categories = ["date-and-time"]
 readme = "README.md"
 license = "Apache-2.0"
-exclude = ["*.tar.gz"]
+exclude = ["*.tar.gz", "data/"]
 edition = "2021"
 
 [lib]
@@ -24,6 +24,9 @@ der = {version = "0.6.1", features = ["derive", "real"], optional = true}
 pyo3 = { version = "0.17.3", features = ["extension-module"], optional = true}
 num-traits = {version = "0.2.15", default-features = false, features = ["libm"]}
 lexical-core = {version = "0.8.5", default-features = false, features = ["parse-integers", "parse-floats"]}
+reqwest = { version = "0.11", features = ["blocking", "json"], optional = true}
+tabled = {version = "0.10.0", optional = true}
+openssl = { version = "0.10", features = ["vendored"], optional = true }
 
 [dev-dependencies]
 serde_json = "1.0.91"
@@ -34,7 +37,8 @@ iai = "0.1"
 default = ["std"]
 std = ["serde", "serde_derive"]
 asn1der = ["der"]
-python = ["std", "asn1der", "pyo3"]
+python = ["std", "asn1der", "pyo3", "ut1"]
+ut1 = ["std", "reqwest", "tabled", "openssl"]
 
 [[bench]]
 name = "bench_epoch"

README.md

@@ -292,7 +292,12 @@ Thanks again to [@gwbres](https://github.com/gwbres) for his work in this releas
 + Fix CI of the formal verification and upload artifacts, cf. [#179](https://github.com/nyx-space/hifitime/pull/179)
 + Introduce time of week construction and conversion by [@gwbres](https://github.com/gwbres), cf.[#180](https://github.com/nyx-space/hifitime/pull/180) and [#188](https://github.com/nyx-space/hifitime/pull/188)
 + Fix minor typo in `src/timeunits.rs` by [@gwbres](https://github.com/gwbres), cf. [#189](https://github.com/nyx-space/hifitime/pull/189)
-+ Significantly extend formal verification of `Duration` and `Epoch`, and introduce `kani::Arbitrary` to `Duration` and `Epoch` for others to formally verify their use of time, cf. [#192](https://github.com/nyx-space/hifitime/pull/192)
++ Significantly extend formal verification of `Duration` and `Epoch`, and introduce `kani::Arbitrary` to `Duration` and `Epoch` for users to formally verify their use of time, cf. [#192](https://github.com/nyx-space/hifitime/pull/192)
++ It is now possible to specify a Leap Seconds file (in IERS format) using the `LeapSecondsFile::from_path` (requires the `std` feature to read the file), cf. [#43](https://github.com/nyx-space/hifitime/issues/43).
++ UT1 time scale is now supported! You must build a `Ut1Provider` structure with data from the JPL Earth Orientation Parameters, or just use `Ut1Provider::download_short_from_jpl()` to automatically download the data from NASA JPL.
++ `strptime` and `strftime` equivalents from C89 are now supported, cf. [#181](https://github.com/nyx-space/hifitime/issues/181). Please refer to the [documentation](https://docs.rs/hifitime/latest/hifitime/efmt/format/struct.Format.html) for important limitations and how to build a custom formatter.
++ ISO Day of Year and Day In Year are now supported for initialization of an Epoch (provided a time scale and a year), and formatting, cf. [#182](https://github.com/nyx-space/hifitime/issues/182).
++ **Python:** the representation of an epoch is now in the time scale it was initialized in
 
 ## 3.7.0
 Huge thanks to [@gwbres](https://github.com/gwbres) who put in all of the work for this release. These usability changes allow [Rinex](https://crates.io/crates/rinex) to use hifitime, check out this work.

data/leap-seconds.list

@@ -0,0 +1,255 @@
+#
+#	In the following text, the symbol '#' introduces
+#	a comment, which continues from that symbol until
+#	the end of the line. A plain comment line has a
+#	whitespace character following the comment indicator.
+#	There are also special comment lines defined below.
+#	A special comment will always have a non-whitespace
+#	character in column 2.
+#
+#	A blank line should be ignored.
+#
+#	The following table shows the corrections that must
+#	be applied to compute International Atomic Time (TAI)
+#	from the Coordinated Universal Time (UTC) values that
+#	are transmitted by almost all time services.
+#
+#	The first column shows an epoch as a number of seconds
+#	since 1 January 1900, 00:00:00 (1900.0 is also used to
+#	indicate the same epoch.) Both of these time stamp formats
+#	ignore the complexities of the time scales that were
+#	used before the current definition of UTC at the start
+#	of 1972. (See note 3 below.)
+#	The second column shows the number of seconds that
+#	must be added to UTC to compute TAI for any timestamp
+#	at or after that epoch. The value on each line is
+#	valid from the indicated initial instant until the
+#	epoch given on the next one or indefinitely into the
+#	future if there is no next line.
+#	(The comment on each line shows the representation of
+#	the corresponding initial epoch in the usual
+#	day-month-year format. The epoch always begins at
+#	00:00:00 UTC on the indicated day. See Note 5 below.)
+#
+#	Important notes:
+#
+#	1. Coordinated Universal Time (UTC) is often referred to
+#	as Greenwich Mean Time (GMT). The GMT time scale is no
+#	longer used, and the use of GMT to designate UTC is
+#	discouraged.
+#
+#	2. The UTC time scale is realized by many national
+#	laboratories and timing centers. Each laboratory
+#	identifies its realization with its name: Thus
+#	UTC(NIST), UTC(USNO), etc. The differences among
+#	these different realizations are typically on the
+#	order of a few nanoseconds (i.e., 0.000 000 00x s)
+#	and can be ignored for many purposes. These differences
+#	are tabulated in Circular T, which is published monthly
+#	by the International Bureau of Weights and Measures
+#	(BIPM). See www.bipm.org for more information.
+#
+#	3. The current definition of the relationship between UTC
+#	and TAI dates from 1 January 1972. A number of different
+#	time scales were in use before that epoch, and it can be
+#	quite difficult to compute precise timestamps and time
+#	intervals in those "prehistoric" days. For more information,
+#	consult:
+#
+#		The Explanatory Supplement to the Astronomical
+#		Ephemeris.
+#	or
+#		Terry Quinn, "The BIPM and the Accurate Measurement
+#		of Time," Proc. of the IEEE, Vol. 79, pp. 894-905,
+#		July, 1991. <http://dx.doi.org/10.1109/5.84965>
+#		reprinted in:
+#		   Christine Hackman and Donald B Sullivan (eds.)
+#		   Time and Frequency Measurement
+#		   American Association of Physics Teachers (1996)
+#		   <http://tf.nist.gov/general/pdf/1168.pdf>, pp. 75-86
+#
+#	4. The decision to insert a leap second into UTC is currently
+#	the responsibility of the International Earth Rotation and
+#	Reference Systems Service. (The name was changed from the
+#	International Earth Rotation Service, but the acronym IERS
+#	is still used.)
+#
+#	Leap seconds are announced by the IERS in its Bulletin C.
+#
+#	See www.iers.org for more details.
+#
+#	Every national laboratory and timing center uses the
+#	data from the BIPM and the IERS to construct UTC(lab),
+#	their local realization of UTC.
+#
+#	Although the definition also includes the possibility
+#	of dropping seconds ("negative" leap seconds), this has
+#	never been done and is unlikely to be necessary in the
+#	foreseeable future.
+#
+#	5. If your system keeps time as the number of seconds since
+#	some epoch (e.g., NTP timestamps), then the algorithm for
+#	assigning a UTC time stamp to an event that happens during a positive
+#	leap second is not well defined. The official name of that leap
+#	second is 23:59:60, but there is no way of representing that time
+#	in these systems.
+#	Many systems of this type effectively stop the system clock for
+#	one second during the leap second and use a time that is equivalent
+#	to 23:59:59 UTC twice. For these systems, the corresponding TAI
+#	timestamp would be obtained by advancing to the next entry in the
+#	following table when the time equivalent to 23:59:59 UTC
+#	is used for the second time. Thus the leap second which
+#	occurred on 30 June 1972 at 23:59:59 UTC would have TAI
+#	timestamps computed as follows:
+#
+#	...
+#	30 June 1972 23:59:59 (2287785599, first time):	TAI= UTC + 10 seconds
+#	30 June 1972 23:59:60 (2287785599,second time):	TAI= UTC + 11 seconds
+#	1  July 1972 00:00:00 (2287785600)		TAI= UTC + 11 seconds
+#	...
+#
+#	If your system realizes the leap second by repeating 00:00:00 UTC twice
+#	(this is possible but not usual), then the advance to the next entry
+#	in the table must occur the second time that a time equivalent to
+#	00:00:00 UTC is used. Thus, using the same example as above:
+#
+#	...
+#       30 June 1972 23:59:59 (2287785599):		TAI= UTC + 10 seconds
+#       30 June 1972 23:59:60 (2287785600, first time):	TAI= UTC + 10 seconds
+#       1  July 1972 00:00:00 (2287785600,second time):	TAI= UTC + 11 seconds
+#	...
+#
+#	in both cases the use of timestamps based on TAI produces a smooth
+#	time scale with no discontinuity in the time interval. However,
+#	although the long-term behavior of the time scale is correct in both
+#	methods, the second method is technically not correct because it adds
+#	the extra second to the wrong day.
+#
+#	This complexity would not be needed for negative leap seconds (if they
+#	are ever used). The UTC time would skip 23:59:59 and advance from
+#	23:59:58 to 00:00:00 in that case. The TAI offset would decrease by
+#	1 second at the same instant. This is a much easier situation to deal
+#	with, since the difficulty of unambiguously representing the epoch
+#	during the leap second does not arise.
+#
+#	Some systems implement leap seconds by amortizing the leap second
+#	over the last few minutes of the day. The frequency of the local
+#	clock is decreased (or increased) to realize the positive (or
+#	negative) leap second. This method removes the time step described
+#	above. Although the long-term behavior of the time scale is correct
+#	in this case, this method introduces an error during the adjustment
+#	period both in time and in frequency with respect to the official
+#	definition of UTC.
+#
+#	Questions or comments to:
+#		Judah Levine
+#		Time and Frequency Division
+#		NIST
+#		Boulder, Colorado
+#		[email protected]
+#
+#	Last Update of leap second values:   8 July 2016
+#
+#	The following line shows this last update date in NTP timestamp
+#	format. This is the date on which the most recent change to
+#	the leap second data was added to the file. This line can
+#	be identified by the unique pair of characters in the first two
+#	columns as shown below.
+#
+#$	 3676924800
+#
+#	The NTP timestamps are in units of seconds since the NTP epoch,
+#	which is 1 January 1900, 00:00:00. The Modified Julian Day number
+#	corresponding to the NTP time stamp, X, can be computed as
+#
+#	X/86400 + 15020
+#
+#	where the first term converts seconds to days and the second
+#	term adds the MJD corresponding to the time origin defined above.
+#	The integer portion of the result is the integer MJD for that
+#	day, and any remainder is the time of day, expressed as the
+#	fraction of the day since 0 hours UTC. The conversion from day
+#	fraction to seconds or to hours, minutes, and seconds may involve
+#	rounding or truncation, depending on the method used in the
+#	computation.
+#
+#	The data in this file will be updated periodically as new leap
+#	seconds are announced. In addition to being entered on the line
+#	above, the update time (in NTP format) will be added to the basic
+#	file name leap-seconds to form the name leap-seconds.<NTP TIME>.
+#	In addition, the generic name leap-seconds.list will always point to
+#	the most recent version of the file.
+#
+#	This update procedure will be performed only when a new leap second
+#	is announced.
+#
+#	The following entry specifies the expiration date of the data
+#	in this file in units of seconds since the origin at the instant
+#	1 January 1900, 00:00:00. This expiration date will be changed
+#	at least twice per year whether or not a new leap second is
+#	announced. These semi-annual changes will be made no later
+#	than 1 June and 1 December of each year to indicate what
+#	action (if any) is to be taken on 30 June and 31 December,
+#	respectively. (These are the customary effective dates for new
+#	leap seconds.) This expiration date will be identified by a
+#	unique pair of characters in columns 1 and 2 as shown below.
+#	In the unlikely event that a leap second is announced with an
+#	effective date other than 30 June or 31 December, then this
+#	file will be edited to include that leap second as soon as it is
+#	announced or at least one month before the effective date
+#	(whichever is later).
+#	If an announcement by the IERS specifies that no leap second is
+#	scheduled, then only the expiration date of the file will
+#	be advanced to show that the information in the file is still
+#	current -- the update time stamp, the data and the name of the file
+#	will not change.
+#
+#	Updated through IERS Bulletin C64
+#	File expires on:  28 June 2023
+#
+#@	3896899200
+#
+2272060800	10	# 1 Jan 1972
+2287785600	11	# 1 Jul 1972
+2303683200	12	# 1 Jan 1973
+2335219200	13	# 1 Jan 1974
+2366755200	14	# 1 Jan 1975
+2398291200	15	# 1 Jan 1976
+2429913600	16	# 1 Jan 1977
+2461449600	17	# 1 Jan 1978
+2492985600	18	# 1 Jan 1979
+2524521600	19	# 1 Jan 1980
+2571782400	20	# 1 Jul 1981
+2603318400	21	# 1 Jul 1982
+2634854400	22	# 1 Jul 1983
+2698012800	23	# 1 Jul 1985
+2776982400	24	# 1 Jan 1988
+2840140800	25	# 1 Jan 1990
+2871676800	26	# 1 Jan 1991
+2918937600	27	# 1 Jul 1992
+2950473600	28	# 1 Jul 1993
+2982009600	29	# 1 Jul 1994
+3029443200	30	# 1 Jan 1996
+3076704000	31	# 1 Jul 1997
+3124137600	32	# 1 Jan 1999
+3345062400	33	# 1 Jan 2006
+3439756800	34	# 1 Jan 2009
+3550089600	35	# 1 Jul 2012
+3644697600	36	# 1 Jul 2015
+3692217600	37	# 1 Jan 2017
+#
+#	the following special comment contains the
+#	hash value of the data in this file computed
+#	use the secure hash algorithm as specified
+#	by FIPS 180-1. See the files in ~/pub/sha for
+#	the details of how this hash value is
+#	computed. Note that the hash computation
+#	ignores comments and whitespace characters
+#	in data lines. It includes the NTP values
+#	of both the last modification time and the
+#	expiration time of the file, but not the
+#	white space on those lines.
+#	the hash line is also ignored in the
+#	computation.
+#
+#h 	2c413af9 124e1031 f165174 ff527c6b 756ae00b

src/efmt/consts.rs

@@ -176,7 +176,7 @@ pub const RFC3339: Format = Format {
         Some(Item {
             token: Token::Second,
             sep_char: Some('.'),
-            second_sep_char: Some('Z'),
+            second_sep_char: None,
             optional: false,
         }),
         Some(Item {

src/efmt/format.rs

@@ -185,6 +185,10 @@ impl Format {
                         ts = TimeScale::from_str(s[idx..].trim())?;
                     }
                     break;
+                } else if char == 'Z' {
+                    // This is a single character to represent UTC
+                    // UTC is the default time scale, so we don't need to do anything.
+                    break;
                 }
                 prev_item = cur_item;
                 prev_token = cur_token;