atspkg
atspkg copied to clipboard
vmchale
language-ats-1.7.6.1: hydra fails on tests
Tests for language-ats 17.6.1 are broken in hydra. It seems to me that test failure is legit:
Failures:
src/Test/Hspec/Dirstream.hs:143:5:
1) pretty-print test/data/wc2.dats
expected: Right "Up to date\nstaload \"SATS/wc.sats\"\nstaload \"SATS/memchr.sats\"\nstaload \"SATS/bytecount.sats\"\nstaload \"prelude/SATS/pointer.sats\"\nstaload UN = \"prelude/SATS/unsafe.sats\"\n\n#include \"DATS/bytecount.dats\"\n#include \"DATS/memchr.dats\"\n\n#define BUFSZ 32768\n\n%{\nsize_t sub_ptr1_ptr1_size(atstype_ptr p1, atstype_ptr p2) {\n return ((char *)p1 - (char *)p2);\n}\n%}\n\nextern\nfn sub_ptr1_ptr1_size { l0, l1 : addr | l0 >= l1 }( p1 : ptr(l0)\n , p2 : ptr(l1)\n ) :<> size_t(l0-l1) =\n \"ext#\"\n\nextern\ncastfn bounded(size_t) : [n:nat] size_t(n)\n\nfn bptr_succ {l:addr}(p : ptr(l)) :<> ptr(l+1) =\n $UN.cast(ptr1_succ<byte>(p))\n\nfn freadc\n{ l : addr | l != null }{ sz : nat | sz >= 1 }(pf : !bytes_v(l, sz)\n | inp : !FILEptr1, bufsize : size_t(sz), p : ptr(l)) : size_t =\n let\n extern\n castfn as_fileref(x : !FILEptr1) :<> FILEref\n \n var n = $extfcall( size_t\n , \"fread\"\n , p\n , sizeof<byte>\n , bufsize\n , as_fileref(inp)\n )\n in\n n\n end\n\nfn freadc_\n{ l : addr | l != null }{ sz : nat | sz >= 1 }{ n : nat | n <= sz }( pf : !bytes_v(l, sz)\n | inp : !FILEptr1\n , bufsize : size_t(sz)\n , p : ptr(l)\n ) : size_t(n) =\n $UN.cast(freadc(pf | inp, bufsize, p))\n\nimplement free_st (st) =\n case+ st of\n | ~in_string () => ()\n | ~in_block_comment () => ()\n | ~line_comment() => ()\n | ~post_asterisk_in_block_comment() => ()\n | ~post_backslash_in_string() => ()\n | ~post_slash() => ()\n | ~regular() => ()\n | ~post_newline_whitespace() => ()\n | ~post_block_comment() => ()\n | ~post_tick() => ()\n\nimplement empty_file =\n @{ lines = 0, blanks = 0, comments = 0, doc_comments = 0 } : file\n\nimplement add_file (f0, f1) =\n @{ lines = f0.lines + f1.lines\n , blanks = f0.blanks + f1.blanks\n , comments = f0.comments + f1.comments\n , doc_comments = f0.doc_comments + f1.doc_comments\n } : file\n\nfn byteview_read_as_char\n{l0:addr}{m:nat}{ l1 : addr | l1 <= l0+m }(pf : !bytes_v(l0, m)\n| p : ptr(l1)) : char =\n $UN.ptr0_get<char>(p)\n\nfn count_for_loop\n{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(pf : !bytes_v(l, m)\n | p : ptr(l), parse_st : &parse_state >> _, bufsz : size_t(n)) :\n file =\n let\n fn advance_char( c : char\n , st : &parse_state >> _\n , file_st : &file >> _\n ) : void =\n case+ st of\n | regular() => \n begin\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.lines := file_st.lines + 1\n ; st := post_newline_whitespace\n )\n | '\\'' => (free(st) ; st := post_tick)\n | '\"' => (free(st) ; st := in_string)\n | '/' => (free(st) ; st := post_slash)\n | _ => ()\n end\n | in_string() => \n begin\n case+ c of\n | '\\n' => file_st.lines := file_st.lines + 1\n | '\\\\' => (free(st) ; st := post_backslash_in_string)\n | '\"' => (free(st) ; st := regular)\n | _ => ()\n end\n | post_asterisk_in_block_comment() => \n begin\n case+ c of\n | '/' => (free(st) ; st := post_block_comment)\n | '\\n' => ( free(st)\n ; file_st.comments := file_st.comments + 1\n ; st := in_block_comment\n )\n | '*' => ()\n | _ => (free(st) ; st := in_block_comment)\n end\n | in_block_comment() => \n begin\n case+ c of\n | '*' => (free(st) ; st := post_asterisk_in_block_comment)\n | '\\n' => file_st.comments := file_st.comments + 1\n | _ => ()\n end\n | line_comment() => \n begin\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.comments := file_st.comments + 1\n ; st := post_newline_whitespace\n )\n | _ => ()\n end\n | post_backslash_in_string() => \n begin\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.lines := file_st.lines + 1\n ; st := in_string\n )\n | _ => ()\n end\n | ~post_slash() => \n begin\n case+ c of\n | '/' => st := line_comment\n | '\\n' => ( file_st.lines := file_st.lines + 1\n ; st := post_newline_whitespace\n )\n | '*' => st := in_block_comment\n | _ => st := regular\n end\n | post_newline_whitespace() => \n begin\n case+ c of\n | '\\n' => (file_st.blanks := file_st.blanks + 1)\n | '\\t' => ()\n | ' ' => ()\n | '/' => (free(st) ; st := post_slash)\n | '\\'' => (free(st) ; st := post_tick)\n | '\"' => (free(st) ; st := in_string)\n | _ => (free(st) ; st := regular)\n end\n | post_block_comment() => \n begin\n // TODO: block comments at the end of a line\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.comments := file_st.comments + 1\n ; st := post_newline_whitespace\n )\n | '/' => (free(st) ; st := post_slash)\n | '\"' => (free(st) ; st := in_string)\n | _ => ()\n end\n | ~post_tick() => st := regular\n \n var res: file = empty_file\n var i: size_t\n val () = for* { i : nat | i <= m } .<i>. (i : size_t(i)) =>\n (i := bufsz ; i != 0 ; i := i - 1)\n (let\n var current_char = byteview_read_as_char(pf | add_ptr_bsz(p, i))\n in\n advance_char(current_char, parse_st, res)\n end)\n var current_char = byteview_read_as_char(pf | p)\n val () = advance_char(current_char, parse_st, res)\n in\n res\n end\n\nfn count_lines_for_loop\n{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(pf : !bytes_v(l, m)\n | ptr : ptr(l), bufsz : size_t(n)) : int =\n let\n var res: int = 0\n var i: size_t\n val () = for* { i : nat | i <= n } .<n-i>. (i : size_t(i)) =>\n (i := i2sz(0) ; i < bufsz ; i := i + 1)\n (let\n var current_char = byteview_read_as_char(pf | add_ptr_bsz(ptr, i))\n in\n case+ current_char of\n | '\\n' => res := res + 1\n | _ => ()\n end)\n in\n res\n end\n\nfn count_file_for_loop(inp : !FILEptr1) : int =\n let\n val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))\n prval () = pfat := b0ytes2bytes_v(pfat)\n \n fun loop { l : addr | l != null }(pf : !bytes_v(l, BUFSZ)\n | inp : !FILEptr1, p : ptr(l)) : int =\n let\n var file_bytes = freadc(pf | inp, i2sz(BUFSZ), p)\n \n extern\n praxi lt_bufsz {m:nat} (size_t(m)) : [m <= BUFSZ] void\n in\n if file_bytes = 0 then\n 0\n else\n let\n var fb_prf = bounded(file_bytes)\n prval () = lt_bufsz(fb_prf)\n var acc = count_lines_for_loop(pf | p, fb_prf)\n in\n acc + loop(pf | inp, p)\n end\n end\n \n var ret = loop(pfat | inp, p)\n val () = mfree_gc(pfat, pfgc | p)\n in\n ret\n end\n\nfn count_file(inp : !FILEptr1) : file =\n let\n val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))\n prval () = pfat := b0ytes2bytes_v(pfat)\n var init_st: parse_state = post_newline_whitespace\n \n fun loop { l : addr | l != null }(pf : !bytes_v(l, BUFSZ)\n | inp : !FILEptr1, st : &parse_state >> _, p : ptr(l)) : file =\n let\n var file_bytes = freadc(pf | inp, i2sz(BUFSZ), p)\n \n extern\n praxi lt_bufsz {m:nat} (size_t(m)) : [m <= BUFSZ] void\n in\n if file_bytes = 0 then\n empty_file\n else\n let\n var fb_prf = bounded(file_bytes)\n prval () = lt_bufsz(fb_prf)\n var acc = count_for_loop(pf | p, st, fb_prf)\n in\n acc + loop(pf | inp, st, p)\n end\n end\n \n var ret = loop(pfat | inp, init_st, p)\n val () = free(init_st)\n val () = mfree_gc(pfat, pfgc | p)\n in\n ret\n end\n"
but got: Right "staload \"SATS/wc.sats\"\nstaload \"SATS/memchr.sats\"\nstaload \"SATS/bytecount.sats\"\nstaload \"prelude/SATS/pointer.sats\"\nstaload UN = \"prelude/SATS/unsafe.sats\"\n\n#include \"DATS/bytecount.dats\"\n#include \"DATS/memchr.dats\"\n\n#define BUFSZ 32768\n\n%{\nsize_t sub_ptr1_ptr1_size(atstype_ptr p1, atstype_ptr p2) {\n return ((char *)p1 - (char *)p2);\n}\n%}\n\nextern\nfn sub_ptr1_ptr1_size { l0, l1 : addr | l0 >= l1 }( p1 : ptr(l0)\n , p2 : ptr(l1)\n ) :<> size_t(l0-l1) =\n \"ext#\"\n\nextern\ncastfn bounded(size_t) : [n:nat] size_t(n)\n\nfn bptr_succ {l:addr}(p : ptr(l)) :<> ptr(l+1) =\n $UN.cast(ptr1_succ<byte>(p))\n\nfn freadc\n{ l : addr | l != null }{ sz : nat | sz >= 1 }(pf : !bytes_v(l, sz)\n | inp : !FILEptr1, bufsize : size_t(sz), p : ptr(l)) : size_t =\n let\n extern\n castfn as_fileref(x : !FILEptr1) :<> FILEref\n \n var n = $extfcall( size_t\n , \"fread\"\n , p\n , sizeof<byte>\n , bufsize\n , as_fileref(inp)\n )\n in\n n\n end\n\nfn freadc_\n{ l : addr | l != null }{ sz : nat | sz >= 1 }{ n : nat | n <= sz }( pf : !bytes_v(l, sz)\n | inp : !FILEptr1\n , bufsize : size_t(sz)\n , p : ptr(l)\n ) : size_t(n) =\n $UN.cast(freadc(pf | inp, bufsize, p))\n\nimplement free_st (st) =\n case+ st of\n | ~in_string () => ()\n | ~in_block_comment () => ()\n | ~line_comment() => ()\n | ~post_asterisk_in_block_comment() => ()\n | ~post_backslash_in_string() => ()\n | ~post_slash() => ()\n | ~regular() => ()\n | ~post_newline_whitespace() => ()\n | ~post_block_comment() => ()\n | ~post_tick() => ()\n\nimplement empty_file =\n @{ lines = 0, blanks = 0, comments = 0, doc_comments = 0 } : file\n\nimplement add_file (f0, f1) =\n @{ lines = f0.lines + f1.lines\n , blanks = f0.blanks + f1.blanks\n , comments = f0.comments + f1.comments\n , doc_comments = f0.doc_comments + f1.doc_comments\n } : file\n\nfn byteview_read_as_char\n{l0:addr}{m:nat}{ l1 : addr | l1 <= l0+m }(pf : !bytes_v(l0, m)\n| p : ptr(l1)) : char =\n $UN.ptr0_get<char>(p)\n\nfn count_for_loop\n{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(pf : !bytes_v(l, m)\n | p : ptr(l), parse_st : &parse_state >> _, bufsz : size_t(n)) :\n file =\n let\n fn advance_char( c : char\n , st : &parse_state >> _\n , file_st : &file >> _\n ) : void =\n case+ st of\n | regular() => \n begin\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.lines := file_st.lines + 1\n ; st := post_newline_whitespace\n )\n | '\\'' => (free(st) ; st := post_tick)\n | '\"' => (free(st) ; st := in_string)\n | '/' => (free(st) ; st := post_slash)\n | _ => ()\n end\n | in_string() => \n begin\n case+ c of\n | '\\n' => file_st.lines := file_st.lines + 1\n | '\\\\' => (free(st) ; st := post_backslash_in_string)\n | '\"' => (free(st) ; st := regular)\n | _ => ()\n end\n | post_asterisk_in_block_comment() => \n begin\n case+ c of\n | '/' => (free(st) ; st := post_block_comment)\n | '\\n' => ( free(st)\n ; file_st.comments := file_st.comments + 1\n ; st := in_block_comment\n )\n | '*' => ()\n | _ => (free(st) ; st := in_block_comment)\n end\n | in_block_comment() => \n begin\n case+ c of\n | '*' => (free(st) ; st := post_asterisk_in_block_comment)\n | '\\n' => file_st.comments := file_st.comments + 1\n | _ => ()\n end\n | line_comment() => \n begin\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.comments := file_st.comments + 1\n ; st := post_newline_whitespace\n )\n | _ => ()\n end\n | post_backslash_in_string() => \n begin\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.lines := file_st.lines + 1\n ; st := in_string\n )\n | _ => ()\n end\n | ~post_slash() => \n begin\n case+ c of\n | '/' => st := line_comment\n | '\\n' => ( file_st.lines := file_st.lines + 1\n ; st := post_newline_whitespace\n )\n | '*' => st := in_block_comment\n | _ => st := regular\n end\n | post_newline_whitespace() => \n begin\n case+ c of\n | '\\n' => (file_st.blanks := file_st.blanks + 1)\n | '\\t' => ()\n | ' ' => ()\n | '/' => (free(st) ; st := post_slash)\n | '\\'' => (free(st) ; st := post_tick)\n | '\"' => (free(st) ; st := in_string)\n | _ => (free(st) ; st := regular)\n end\n | post_block_comment() => \n begin\n // TODO: block comments at the end of a line\n case+ c of\n | '\\n' => ( free(st)\n ; file_st.comments := file_st.comments + 1\n ; st := post_newline_whitespace\n )\n | '/' => (free(st) ; st := post_slash)\n | '\"' => (free(st) ; st := in_string)\n | _ => ()\n end\n | ~post_tick() => st := regular\n \n var res: file = empty_file\n var i: size_t\n val () = for* { i : nat | i <= m } .<i>. (i : size_t(i)) =>\n (i := bufsz ; i != 0 ; i := i - 1)\n (let\n var current_char = byteview_read_as_char(pf | add_ptr_bsz(p, i))\n in\n advance_char(current_char, parse_st, res)\n end)\n var current_char = byteview_read_as_char(pf | p)\n val () = advance_char(current_char, parse_st, res)\n in\n res\n end\n\nfn count_lines_for_loop\n{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(pf : !bytes_v(l, m)\n | ptr : ptr(l), bufsz : size_t(n)) : int =\n let\n var res: int = 0\n var i: size_t\n val () = for* { i : nat | i <= n } .<n-i>. (i : size_t(i)) =>\n (i := i2sz(0) ; i < bufsz ; i := i + 1)\n (let\n var current_char = byteview_read_as_char(pf | add_ptr_bsz(ptr, i))\n in\n case+ current_char of\n | '\\n' => res := res + 1\n | _ => ()\n end)\n in\n res\n end\n\nfn count_file_for_loop(inp : !FILEptr1) : int =\n let\n val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))\n prval () = pfat := b0ytes2bytes_v(pfat)\n \n fun loop { l : addr | l != null }(pf : !bytes_v(l, BUFSZ)\n | inp : !FILEptr1, p : ptr(l)) : int =\n let\n var file_bytes = freadc(pf | inp, i2sz(BUFSZ), p)\n \n extern\n praxi lt_bufsz {m:nat} (size_t(m)) : [m <= BUFSZ] void\n in\n if file_bytes = 0 then\n 0\n else\n let\n var fb_prf = bounded(file_bytes)\n prval () = lt_bufsz(fb_prf)\n var acc = count_lines_for_loop(pf | p, fb_prf)\n in\n acc + loop(pf | inp, p)\n end\n end\n \n var ret = loop(pfat | inp, p)\n val () = mfree_gc(pfat, pfgc | p)\n in\n ret\n end\n\nfn count_file(inp : !FILEptr1) : file =\n let\n val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))\n prval () = pfat := b0ytes2bytes_v(pfat)\n var init_st: parse_state = post_newline_whitespace\n \n fun loop { l : addr | l != null }(pf : !bytes_v(l, BUFSZ)\n | inp : !FILEptr1, st : &parse_state >> _, p : ptr(l)) : file =\n let\n var file_bytes = freadc(pf | inp, i2sz(BUFSZ), p)\n \n extern\n praxi lt_bufsz {m:nat} (size_t(m)) : [m <= BUFSZ] void\n in\n if file_bytes = 0 then\n empty_file\n else\n let\n var fb_prf = bounded(file_bytes)\n prval () = lt_bufsz(fb_prf)\n var acc = count_for_loop(pf | p, st, fb_prf)\n in\n acc + loop(pf | inp, st, p)\n end\n end\n \n var ret = loop(pfat | inp, init_st, p)\n val () = free(init_st)\n val () = mfree_gc(pfat, pfgc | p)\n in\n ret\n end\n"
To rerun use: --match "/pretty-print/test/data/wc2.dats/"
