Leap for Leap Seconds!

Question

Since today marks the occasion of the 26th leap second ever to occur, your challenge will be to output the date and time of every leap second in GMT or UTC that has occurred so far, as well as the one to occur today.

Input

There is no input.

Output

1972-06-30 23:59:60
1972-12-31 23:59:60
1973-12-31 23:59:60
1974-12-31 23:59:60
1975-12-31 23:59:60
1976-12-31 23:59:60
1977-12-31 23:59:60
1978-12-31 23:59:60
1979-12-31 23:59:60
1981-06-30 23:59:60
1982-06-30 23:59:60
1983-06-30 23:59:60
1985-06-30 23:59:60
1987-12-31 23:59:60
1989-12-31 23:59:60
1990-12-31 23:59:60
1992-06-30 23:59:60
1993-06-30 23:59:60
1994-06-30 23:59:60
1995-12-31 23:59:60
1997-06-30 23:59:60
1998-12-31 23:59:60
2005-12-31 23:59:60
2008-12-31 23:59:60
2012-06-30 23:59:60
2015-06-30 23:59:60

Rules

Since I doubt there are many built-ins that allow leap-seconds, I'll allow them.

Standard loopholes are disallowed.

Shortest code wins.

Date format must have a zero-padded month and a 4-digit year, as well as military time and a space separating the time from the date. Putting UTC at the end is optional. Your choice of dashes or slashes.

EDIT: Yep as predicted, this became an encoding challenge. If only encoding could fix the leap second problem, ...then all our code would be much more practical. Maybe we need some ideas for more fun challenges with practical uses?

Answer 1

CJam, 72 70 69 64 bytes

26,"~g¼K&Béx¸¦­Ø"240bFbf{<1b2md\1972+'-@6X$4*-'-Z3$" 23:59:60"N}

Try it online in the CJam interpreter.

Idea

We start by encoding each leap second as 2 * (Y - 1972) + D, where D is 1 if it occurs in December and 0 otherwise.

The array of all encoded leap seconds is:

[0 1 3 5 7 9 11 13 15 18 20 22 26 31 35 37 40 42 44 47 50 53 67 73 80 86]

Let's call this array L.

Since the array is in ascending order, we can store the consecutive differences instead of the actual numbers:

[1 2 2 2 2 2 2 2 3 2 2 4 5 4 2 3 2 2 3 3 3 14 6 7 6]

Treating this array as the digits of a base 15 number, we obtain the integer

19238985373462115979359619336

which digits in base 240 (cast to characters) are

~g¼K&Béx¸¦­Ø

Code

26,             e# Push I := [0 ... 25].
"~g¼K&Béx¸¦­Ø"   e# Push the string from above.
240bFb          e# Convert from base 250 to base 15 to push L.
f{              e# For each J in I:
                e#   Push L.
  <             e#   Replace L with L[:J].
  1b            e#   Push the sum S of the integers in L[:J].
  2md           e#   Push (S / 2) and (S % 2).
  \1972+        e#   Add 1972 to (S / 2).
  '-@           e#   Push '-' and rotate (S % 2) on top.
  6X$4*-        e#   Compute (6 - 4 * (S % 2)).
  '-Z           e#   Push '-' and 3.
  3$            e#   Push a copy of (S % 2).
  " 23:59:60"   e#   Push that string.
  N             e#   Push a linefeed.
}

Answer 2

R, 78 75 bytes

Built-ins, you say? Well...

message(paste(as.Date(.leap.seconds)-1,"23:59:60\n"),"2015-06-30 23:59:60")

R has an automatic variable .leap.seconds which contains the date and time of each leap second insertion, given in the system's local time. As of R version 3.2.0, this does not include today, so I've added that manually.

Ungolfed + explanation:

# Convert the datetime values to UTC dates. These will be a day past the
# expected output, so we can subtract 1 to get what we want.
dates <- as.Date(.leap.second) - 1

# Paste the UTC time and a newline onto the end of each date
datetimes <- paste(dates, "23:59:60\n")

# Print each time, including today, on its own line
message(datetimes, "2015-06-30 23:59:60")

You can try it online!

Answer 3

HTML, 594 bytes

1972-06-30 23:59:60<br>1972-12-31 23:59:60<br>1973-12-31 23:59:60<br>1974-12-31 23:59:60<br>1975-12-31 23:59:60<br>1976-12-31 23:59:60<br>1977-12-31 23:59:60<br>1978-12-31 23:59:60<br>1979-12-31 23:59:60<br>1981-06-30 23:59:60<br>1982-06-30 23:59:60<br>1983-06-30 23:59:60<br>1985-06-30 23:59:60<br>1987-12-31 23:59:60<br>1989-12-31 23:59:60<br>1990-12-31 23:59:60<br>1992-06-30 23:59:60<br>1993-06-30 23:59:60<br>1994-06-30 23:59:60<br>1995-12-31 23:59:60<br>1997-06-30 23:59:60<br>1998-12-31 23:59:60<br>2005-12-31 23:59:60<br>2008-12-31 23:59:60<br>2012-06-30 23:59:60<br>2015-06-30 23:59:60

¯\_(ツ)_/¯

Answer 4

C, 160 146 141 140 bytes

First time posting, not sure what "standard loopholes" are. I have printf warnings of course.

160 bytes:

The original idea is to encode leap seconds using two bits per year: one for June and one for December. The encoding is consumed one bit at a time by the inner while loop. Without a 128-bit integer, the outer while loop is necessary. The rest is all bookkeeping and math. :-)

int main(){long long X=0x2495288454AAAB,Y=1972,Z=1;while(Y<2000){while(X){if(X&1)printf("%d-%02d-%d 23:59:60\n",Y,6*(2-Z),31-Z);Y+=Z^=1;X>>=1;}X=0x104082000;}}

141 bytes:

Applying the suggested tips gets it down to 146 bytes. Then I found a way to simplify the outer while condition (from Y<2000 to just Z), bringing it down to 141 bytes. So close to a tweet!

main(Z){long long X=0x2495288454AAAB,Y=1972;while(Z){while(X)X&1?printf("%d-%02d-%d 23:59:60\n",Y,12-6*Z,31-Z):1,Y+=Z^=1,X/=2;X=4362608640;}}

140 bytes:

I noticed the dash in the date could be eliminated by making the day negative. Can't do it with the month as well due to leading zero in June. But at least it fits in a tweet now!

main(Z){long long X=0x2495288454AAAB,Y=1972;while(Z){while(X)X&1?printf("%d-%02d%d 23:59:60\n",Y,12-6*Z,Z-31):1,Y+=Z^=1,X/=2;X=4362608640;}}

Pretty version:

main(Z) {
    long long X = 0x2495288454AAAB, Y = 1972;
    while (Z) {
        while (X)
            X&1 ? printf("%d-%02d%d 23:59:60\n", Y, 12-6*Z, Z-31) : 1,
            Y += Z ^= 1,
            X /= 2;
        X = 4362608640;
    }
}

Bonus version:

I eliminated the outer loop by bit-shifting one 64-bit integer into another, but it's 150 bytes, due to the rather long "unsigned long long"; if I could use something like "uint64" it would be 138 bytes.

main(Z) {
    unsigned long long Y = 1972, X = 0x2495288454AAAB, W = 8520720;
    while (X)
        X&1 ? printf("%d-%02d-%d 23:59:60\n", Y, 12-6*Z, 31-Z) : 1,
        Y += Z^= 1,
        X = X/2 | (W>>=1)<<63;
}

Answer 5

Python 3, 91

Uses the encoding and string formatting by Sp3000, but stores the values in a Python 3 bytes object rather than a magic number.

for n in b'()+-/1357:<>BGKMPRTWZ]kqx~':print('%d-%02d-3%d 23:59:60'%(1952+n/2,n%2*6+6,n%2))

The encoding only needs 86 of the 256 possible values of a bytes, so a range of printable characters is used to make it look nicer.

Answer 6

Brainfuck, 806

++++++++[>++++++>+++++++>+++++++>++++++>++++++>++++++>+++++++>++++++>++++++>++++++>++++>++++++>++++++>+++++++>+++++++>+++++++>+++++++>+++++++>++++++>+<<<<<<<<<<<<<<<<<<<<-]>+>+>->++>--->>-->--->+++>>>++>+++>++>--->+>++>-->>++[<]>[.>]<[<]>>>>>>+>---->>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>+>-------->>->++++>>>-[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>++[<]>[.>]<[<]>>>>++>>+>---->>>+[<]>[.>]<[<]>>>>++[<]>[.>]<[<]>>>+>---------[<]>[.>]<[<]>>>>++>>->++++>>>-[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+[<]>[.>]<[<]>>>>+>>+>---->>>+[<]>[.>]<[<]>>>>++>>->++++>>>-[<]>[.>]<[<]>>>>+>>+>---->>>+[<]>[.>]<[<]>+>--------->--------->---[<]>[.>]<[<]>>>>+++[<]>[.>]<[<]>>>+>------>>->++++>>>-[<]>[.>]<[<]>>>>+++[<]>[.>]

You can run it on this online interpreter.

Answer 7

Python 2, 111 104 bytes

n=0x6697f252225354422533333330;y=1972
while n:print'%d-%02d-3%d 23:59:60'%(y,n%2*6+6,n%2);y+=n/2%8;n/=16

Base encoding and more base encoding.

Answer 8

GNU sed+date: 112

Common Linux distributions have the leap seconds built-in, too. Using GNU sed and date:

sed -n 's/^\([0-9]\+\).*/1899-12-31 \1sec/p' /usr/share/zoneinfo/leap-seconds.list|date -f- +"%Y-%m-%d 23:59:60"

GNU sed+date: 90

Safing a few characters by cutting the path:

sed -n 's/^\([0-9]\+\).*/1899-12-31 \1sec/p' /u*/s*/z*/leap*|date -f- +'%Y-%m-%d 23:59:60'

GNU sed+date tuned by Toby Speight: 84

Deeply golfed version proposed in the comments:

sed -nr 's/^([0-9]+).*/date -d "1899-12-31 \1sec" "+%F 23:59:60"/ep' /u*/s*/z*/leap*

Answer 9

JavaScript (ES6) 125

The newline inside `` is significant and counted.

To test, run the snippet below (being EcmaScript 6, Firefox only)

alert([..."09:;=DEFIX[01234567?ABGJQS"].map((c,i)=>c.charCodeAt()+1924+(i>10?'-12-31':'-06-30')+' 23:59:60').sort().join`
`)

Answer 10

PHP, 198 bytes

foreach([.5,1,2,3,4,5,6,7,8,9.5,10.5,11.5,13.5,16,18,19,20.5,21.5,22.5,24,25.5,27,34,37,40.5,43.5] as$d){$h=(int)$d-ceil($d);echo date("Y-m-d 23:59:60",mktime(0,0,0,-6*$h,31+$h,(int)$d+1972))."\n";}

Unfortunately, I don't know if I can insert \n in the date function. If so, this is 3 bytes less because of ."".

Answer 11

8086 machine code + DOS, 92 bytes

Hexdump of the code:

BE 3A 01 B1 57 D1 E0 75 03 AD EB F9 72 09 50 BA
47 01 B4 09 CD 21 58 BB 50 01 81 77 FC 01 04 80
37 01 80 3F 31 74 10 83 EB 05 4B FE 07 80 3F 3A
75 05 C6 07 30 EB F3 E2 CC C3 AA 2A 77 B5 6A DD
DF B6 BE FF 7D BF 31 39 37 32 2D 30 36 2D 33 30
20 32 33 3A 35 39 3A 36 30 0D 0A 24

To run, write the 92 bytes into a com-file and run under 32-bit Windows or DOSBox.

The code uses a bitmap with 87 bits, one per half a year. The bits are arranged into groups of 16, starting from MSB.

Decoding the bitmap:

                 ; when the program starts, ax=0 (tested on DOSBox)
myloop:
    shl ax, 1    ; shift the MSB left into the carry flag
    jnz mywork   ; if some bits are left in the register, work normally
    lodsw        ; if all bits were shifted out, load the next 16 bits
    jmp myloop   ; and check the MSB again

Because of the code's structure, some bits are lost during decoding, so I had to repeat them. This repeating doesn't bloat the bitmap because I had to pad 87 bits to 96 bits anyway.

After printing (or not printing) the leap second, the code increases the date by half a year, using manipulations on the ASCII codes of the output message.

Source code (can be assembled with tasm):

    mov si, offset mydata
    mov cl, 57h ; number of iterations

myloop:
    shl ax, 1   ; shift the MSB left into the carry flag
    jnz mywork  ; if some bits are left in the register, work normally
    lodsw       ; if all bits were shifted out, load the next 16 bits
    jmp myloop  ; and check the MSB again
mywork:
    jc myinc_date ; shifted bit 1? - skip printing the message

    push ax
    mov dx, offset mymsg
    mov ah, 9
    int 21h     ; print the message
    pop ax

myinc_date:
    mov bx, offset mymsg + 9 ; pointer to the middle of the message
    xor word ptr [bx - 4], 401h ; change month 06<->12
    xor byte ptr [bx], 1 ; change day 30<->31
    cmp byte ptr [bx], '1'
    je myloop_end ; if 31 December, no need to increase the year
    sub bx, 5 ; pointer beyond the last digit of the year

myinc_year:
    dec bx
    inc byte ptr [bx] ; increase the digit
    cmp byte ptr [bx], '0' + 10
    jne myloop_end ; if the digit was less than 9, done
    mov byte ptr [bx], '0' ; set the digit to 0
    jmp myinc_year ; continue increasing other digits

myloop_end:
    loop myloop
    ret ; terminate the program

; In the following bitmap, the spaces before some LSBs
; show that the least significant 1-bit and all
; following 0-bits are lost during decoding.
mydata:
    dw 02aaah ; 00101010101010     10
    dw 0b577h ; 101101010111011    1
    dw 0dd6ah ; 11011101011010     10
    dw 0b6dfh ; 101101101101111    1
    dw 0ffbeh ; 11111111101111     10
    dw 0bf7dh ; 101111110111110    1

mymsg:
    db '1972-06-30 23:59:60',13,10,'$'

Answer 12

Python 2, 123 121 116 114 111

I've managed to get it pretty short, but I'm not sure how much shorter it can get. I tried using exec, but the formatting gets to be too costly.

I used a base 16 encoding of the table from the linked Wikipedia page.

Edit: Using hex encoding is shorter than base 36 (see the less golfed version.)

Try it here

n=0x410208002495288454aaab
for i in range(88):
    if n%2:print"%d-%02d-3%d 23:59:60"%(1972+i/2,i%2*6+6,i%2)
    n/=2

Less golfed:

s=bin(int('WELD24ZDGIMBWWLFM',36))[2:]
for i in range(44):
    t,s=int(s[0]),s[1:]
    if t:print"%d-06-30 23:59:60"%(i+1972)
    t,s=int(s[0]),s[1:]
    if t:print"%d-12-31 23:59:60"%(i+1972)

Answer 13

Pyth - 88 84 bytes

Converts to char to compress the data and saves the 06-30 versus 12-31 data as binary number.

jbm++-2047ed?"-06-30"hd"-12-31"" 23:59:60"C,j33678243 2CM"KKJIHGFEDBA@><:9765421*'# 

(there is a space there at the end)

Try it here online.

Answer 14

Python, 204 201

e,g,h=0,1972,0
for i in range(1,27):e,g,h={2:1,9:2,10:1,12:2,15:1,16:2,17:1,20:2,21:1,22:7,23:3,24:4,25:3}.get(i,e),g+e,(h,1-h)[i in[2,10,14,17,20,21,22,25]];print`g`+("-06-30","-12-31")[h]+" 23:59:60"

You can play with it on repl.it.

Edit: Thoroughly beaten! The compression answers are amazingly short.

Answer 15

q/kdb+, 95 94 93 bytes

asc 1_" "0:([]raze("DEFGHIJKSUV[^eh";"DMNOQXYZ]lo"){("d"$"m"$-12*95-6h$x)-y}'1 185;`23:59:60)

Explanation

For each year + 1, encode for years since 1905 as an ASCII character, e.g.:

1972 -> 1973 -> 68 -> D

6h$x turns "D" back to 68. Since q's date epoch is 2000.01.01, we subtract 95 and perform the integers-to-date conversion "d"$"m"$-12*95-6h$x.

The reason we + 1 above is to subtract the number of days from the start of next year to get the actual year's 31st December or 30th June, namely 1 or 185 days. Therefore, "DEFGHIJKSUV[^eh" represents the years with a leap second in December, and "DMNOQXYZ]lo" for those in June. The pairing-subtraction is done via (a;b){x-y}'(c;d), where a and b are years that will be subtracted by c and d number of days respectively.

" "0:([]...) prepares the results to give us the correct formatting, with a small caveat that a column header will be generated. 1_ drops that header and finally apply asc to get the ordering correct.

edit: 're-base' to subtracting 95 years instead of 100 (saving 1 character).

edit 2: re-ordering the operands' positioning inside the integers-to-date conversion function.

Answer 16

C, 155 149 147 bytes

Here's another approach in C, using strings and run length encoding. Not quite as terse as my other C solution, but maybe it can be improved?

155 bytes:

Using a string to hold the month/day.

main(Y){Y=1972;char*M="06-3012-31",*B="#@DGCDF7D3daTdS#!",b,c;while(b=*B++-33){c=b>>1&7;while(c--)printf("%d-%.5s 23:59:60\n",Y++,M+b%2*5);Y+=(b>>4&7)-1;}}

149 bytes:

Eliminating the month/day string.

main(Y){Y=1972;char*B="#@DGCDF7D3daTdS#!",b,c;while(b=*B++-33){c=b>>1&7;while(c--)printf("%d-%02d-%d 23:59:60\n",Y++,6+b%2*6,30+b%2);Y+=(b>>4&7)-1;}}

147 bytes:

Eliminating the year initialization.

main(Y){char*B="#@DGCDF7D3daTdS#!",b,c;while(b=*B++-33){c=b>>1&7;while(c--)printf("%d-%02d-%d 23:59:60\n",1971+Y++,6+b%2*6,30+b%2);Y+=(b>>4&7)-1;}}

144 bytes:

If I reencoded the buffer to make the skip count apply before (not after) the run, then I could reorder the statements in the outer while loop, use the comma operator, and eliminate the braces, saving 2 bytes.

I can save another byte by making the day negative (as in my other solution).

Pretty:

main(Y) {
    char *B = "#@DGCDF7D3daTdS#!", // buffer of bytes encoding runs
         b, // current byte
         c; // current count
    while (b = *B++-33) { // get byte
        c = b>>1&7; // get count
        while (c--) printf("%d-%02d-%d 23:59:60\n", 1971+Y++, 6+b%2*6, 30+b%2); // run
        Y += (b>>4&7)-1; // skip years
    }
}

Explanation:

Runs are encoded in bytes. Each byte has one bit to say whether it's June or December, 3 bits for a length count, 3 bits for a skip count, and 1 unused high bit.

The skip count is the number of years to skip after a run; it's offset by -1 to allow for two leap seconds in 1972. The length is how many years in a run; it probably could be offset by +1 but it isn't currently.

So a byte means: "Do LENGTH years of JUNE (or DECEMBER) years of leap seconds, then skip SKIP-1 years" before moving to the next byte.

The bytes are offset by 33 to make them readable and avoid fancy encoding.

This means although we have enough skip bits to cover 1998-2005, we're out of ASCII range, so we have an extra zero length run. Also, 1979 appears on its own because the length 1972-1979 is one too long.

There's enough bits in the bytes, so those issues might be fixable ultimately.

Answer 17

Python, 221 217

def d(x):
 q=x%10
 if x%2==0:
  p,r=q/2,"06-30"
 else:
  p,r=(q-1)/2,"12-31"
 return"%d%d-%s 23:59:60"%(p+197,x/10,r)
for x in [20,21,31,41,51,61,71,81,91,12,22,32,52,73,93,5,24,34,44,55,74,85,57,87,28,58]:print(d(x))

Some Insights

Basically, d(x) decompresses a vector of 3 integers from a single 2-digit integer. d(x) is constructed as the inverse function (over the 26 leap seconds datetimes) of c(v), which in turn is a compression function that turns a 3-uple such as (1998,12,31) into a number like 85. To derive the list [20,21...28,58] I designed another algorithm to verify that the compression function is bijective over the domain. That is, I made sure that the following program doesn't produce duplicates, and I used its output as the list of the program above.

dates = [(1972,06,30),
    (1972,12,31),
    (1973,12,31),
    (1974,12,31),
    (1975,12,31),
    (1976,12,31),
    (1977,12,31),
    (1978,12,31),
    (1979,12,31),
    (1981,06,30),
    (1982,06,30),
    (1983,06,30),
    (1985,06,30),
    (1987,12,31),
    (1989,12,31),
    (1990,12,31),
    (1992,06,30),
    (1993,06,30),
    (1994,06,30),
    (1995,12,31),
    (1997,06,30),
    (1998,12,31),
    (2005,12,31),
    (2008,12,31),
    (2012,06,30),
    (2015,06,30)]

def c(v):
    x = (v[0] % 10) * 10
    x += v[2] % 30
    x += 2 * (int(v[0] / 10) - 197)
    return x

for v in dates:
    print(c(v))

The compression function c(v) was designed to be bijective by using a very simple scheme. Let's take as an example (1998,12,31).

• The expression (v[0] % 10) * 10 selects the units of the year (e.g. 1 9 9 8 --> 8) and makes it the tenths digit of the output (now x=80).
• There are only two month-day combination in which the leap second thing happens, so I decided to use the day component to distinguish between the 06,30 case and the 12,31 case. The expression v[2] % 30 is 0 if the day is 30, and is 1 if the day is 31. In our example, we add 1 to x (hence, now x=81).
• Finally, I observed that this puzzle involves only 5 decades; hence if I map the first decade (the seventies) to 0 and the last decade (the 2010s) to 4 I can do cool stuff. More specifically, if instead of mapping to 0,1,2,3,4 I map to 0,2,4,6,8 I can add this value to the units of x, which due to the previous rule is either 0 or 1. So in the end we have that also this last step doesn't screw the bijection, and we get that the units of a 06,30 case are one of 0,2,4,6,8 and that the units of a 12,31 case are one of 1,3,5,7,9. Hence the bijection is obvious. In our example, 1998 is in the third decade (70s->0, 80s->1, 90s->2) so we add 2*2=4. So we get x=85.

I wrote the program to verify that this is true, and then I defined d(x) as the inverse of c(v). In our example, c((1998,12,31)) is 85 and d(85) correctly prints 1998-12-31 23:59:60.

Answer 18

PHP, 164 bytes

foreach([.5,1,2,3,4,5,6,7,8,9.5,10.5,11.5,13.5,16,18,19,20.5,21.5,22.5,24,25.5,27,34,37,40.5,43.5]as$d){echo(ceil($d)+1971).($d%2?'-12-31':'-06-30')." 23:59:60\n";}

This is just a few modification on @Voitcus's idea

Answer 19

gzip, 114 bytes

Hexdump:

1f8b080853f9975502006c006dd04b0a80300c84e1bde01dbc40218fa6697aff8309e2a6fa6f3f86cc10adb426a3b95ce62b6a0d398f07d59aeb8e4ed80983701026e1242cc0a9307e1aa11306615211b59710527b3961270cba9994fc7fc944829092faeedc313e7803993cfafb20020000

Create a file with the bytes described above.

Extract using gunzip or another decompression program to get a new file named "l". This file contains the desired output.