Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.
Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.
Maybe we can even convene again some time?
I once worked on a theorem-proving project and we spent a LOT of time
on prettifying the output of our theorem-prover. This somewhat traumatizing
experience taught me to be wary of pretty-printing.
ah, ok, good point then – actual experience! 
here’s me w/out that experience, as a newbie, thinking: anything that
can be written as actual mathematical symbols (e.g. “illegal: 1 + x ==
x”) rather than as the names used internally by the solver etc. would
be better UI/UX i think.
i guess i hope there’s a way to do something like that but to do it in
light of your experiences? where do you think it went off track? are
there small wins that could be attained if not for ‘solving’ the whole
question?
Thank you very much, I’m glad you liked it. It was really good getting some
feed back on ATS and the good suggestions on usability. I plan to
(hopefully) work some of them into an external constraint solver. In any
case, pretty printing unsolved constraints is high on my priority list :D.
I’m working on annotating the code we went through, and I’ll post it to
this thread when it’s done.On Thursday, August 14, 2014 12:44:31 AM UTC-4, Raoul Duke wrote:
Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.Maybe we can even convene again some time?
one thing i thought while following the tutorial was that it’d be really
useful to have a pretty printer for the constraint solver error messages.
is this something it would be feasible to do as an external project, on a
purely text-transformation basis? if so i’d be happy to have a go at it (if
it requires plugging into the guts of ats i probably won’t have much
chance, but text->text seems like it’d be mostly a matter of putting the
work in)
martinOn Fri, Aug 15, 2014 at 12:20 PM, William Blair < william.dou...@gmail.com> wrote:
Thank you very much, I’m glad you liked it. It was really good getting
some feed back on ATS and the good suggestions on usability. I plan to
(hopefully) work some of them into an external constraint solver. In any
case, pretty printing unsolved constraints is high on my priority list :D.I’m working on annotating the code we went through, and I’ll post it to
this thread when it’s done.On Thursday, August 14, 2014 12:44:31 AM UTC-4, Raoul Duke wrote:
Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.Maybe we can even convene again some time?
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com?utm_medium=email&utm_source=footer
.
now i can only think of A Clockwork Orange…
Great, I’ll take a look at it
martinOn Fri, Aug 15, 2014 at 1:12 PM, William Blair < william.dou...@gmail.com> wrote:
It is feasible to do now that the ATS compiler can export constraints in a
JSON format. One issue is that it exports all of the constraints in the
program into one big JSON object. We have been working on an external
constraint solver that uses this format as input. I need to clean the code
up a bit so that others can contribute and use it, but the task of pretty
printing in it shouldn’t be that difficult.If you’d like to inspect constraints in JSON, you can do the following:
patsopt --constraint-export -tc -d foo.dats | python -m json.tool >foo.json
and you’ll get nice formatted output.
On Friday, August 15, 2014 3:59:26 PM UTC-4, Martin DeMello wrote:
one thing i thought while following the tutorial was that it’d be really
useful to have a pretty printer for the constraint solver error messages.
is this something it would be feasible to do as an external project, on a
purely text-transformation basis? if so i’d be happy to have a go at it (if
it requires plugging into the guts of ats i probably won’t have much
chance, but text->text seems like it’d be mostly a matter of putting the
work in)martin
On Fri, Aug 15, 2014 at 12:20 PM, William Blair <william...@gmail.com wrote:
Thank you very much, I’m glad you liked it. It was really good getting
some feed back on ATS and the good suggestions on usability. I plan to
(hopefully) work some of them into an external constraint solver. In any
case, pretty printing unsolved constraints is high on my priority list :D.I’m working on annotating the code we went through, and I’ll post it to
this thread when it’s done.On Thursday, August 14, 2014 12:44:31 AM UTC-4, Raoul Duke wrote:
Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.Maybe we can even convene again some time?
–
You received this message because you are subscribed to the Google
Groups “ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send
an email to ats-lang...@googlegroups.com.
To post to this group, send email to ats-l...@googlegroups.com.Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/
msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%
40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com?utm_medium=email&utm_source=footer
.–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/1032f361-4cfb-4aa3-b2dd-e63fc947caf9%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/1032f361-4cfb-4aa3-b2dd-e63fc947caf9%40googlegroups.com?utm_medium=email&utm_source=footer
.
For now, a simple document telling people how to read the type-error
messages should be very helpful.
For instance, the following line of code
val () = assertloc (sum = showtype(1+2+3+4+5.0))
generates the following messages:
/tmp/abcde.dats: 357(line=27, offs=10) – 394(line=27, offs=47): error(3):
the symbol [=] cannot be resolved as no match is found.
/tmp/abcde.dats: 357(line=27, offs=10) – 394(line=27, offs=47): error(3):
[/home/hwxi/research/Postiats/git/src/pats_trans3_util.dats]: d3exp_trdn:
the dynamic expression cannot be assigned the type
[S2Eapp(S2Ecst(bool_bool_t0ype); S2EVar(10))].
/tmp/abcde.dats: 357(line=27, offs=10) – 394(line=27, offs=47): error(3):
mismatch of static terms (tyleq):
It means:
I think such a document would be far more useful than pretty-printing
constraints at this point.On Friday, August 15, 2014 3:59:26 PM UTC-4, Martin DeMello wrote:
one thing i thought while following the tutorial was that it’d be really
useful to have a pretty printer for the constraint solver error messages.
is this something it would be feasible to do as an external project, on a
purely text-transformation basis? if so i’d be happy to have a go at it (if
it requires plugging into the guts of ats i probably won’t have much
chance, but text->text seems like it’d be mostly a matter of putting the
work in)martin
On Fri, Aug 15, 2014 at 12:20 PM, William Blair <william...@gmail.com <javascript:>> wrote:
Thank you very much, I’m glad you liked it. It was really good getting
some feed back on ATS and the good suggestions on usability. I plan to
(hopefully) work some of them into an external constraint solver. In any
case, pretty printing unsolved constraints is high on my priority list :D.I’m working on annotating the code we went through, and I’ll post it to
this thread when it’s done.On Thursday, August 14, 2014 12:44:31 AM UTC-4, Raoul Duke wrote:
Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.Maybe we can even convene again some time?
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com?utm_medium=email&utm_source=footer
.
I think such a document would be far more useful than pretty-printing
constraints at this point.
Is this because the format of the constraints might change? Otherwise
I cannot agree
It is feasible to do now that the ATS compiler can export constraints in a
JSON format. One issue is that it exports all of the constraints in the
program into one big JSON object. We have been working on an external
constraint solver that uses this format as input. I need to clean the code
up a bit so that others can contribute and use it, but the task of pretty
printing in it shouldn’t be that difficult.
If you’d like to inspect constraints in JSON, you can do the following:
patsopt --constraint-export -tc -d foo.dats | python -m json.tool >
foo.json
and you’ll get nice formatted output.On Friday, August 15, 2014 3:59:26 PM UTC-4, Martin DeMello wrote:
one thing i thought while following the tutorial was that it’d be really
useful to have a pretty printer for the constraint solver error messages.
is this something it would be feasible to do as an external project, on a
purely text-transformation basis? if so i’d be happy to have a go at it (if
it requires plugging into the guts of ats i probably won’t have much
chance, but text->text seems like it’d be mostly a matter of putting the
work in)martin
On Fri, Aug 15, 2014 at 12:20 PM, William Blair <william...@gmail.com <javascript:>> wrote:
Thank you very much, I’m glad you liked it. It was really good getting
some feed back on ATS and the good suggestions on usability. I plan to
(hopefully) work some of them into an external constraint solver. In any
case, pretty printing unsolved constraints is high on my priority list :D.I’m working on annotating the code we went through, and I’ll post it to
this thread when it’s done.On Thursday, August 14, 2014 12:44:31 AM UTC-4, Raoul Duke wrote:
Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.Maybe we can even convene again some time?
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/26a4910b-8f33-4f11-ae40-722c8e410a6f%40googlegroups.com?utm_medium=email&utm_source=footer
.
You will get used to it if you stare it long enough
I can tell you that I have stared at Python’s syntax for quite some time
recently.On Friday, August 15, 2014 2:31:48 PM UTC-4, Raoul Duke wrote:
I think if Will posts his annotated code that he worked on during the
tutorial session, that will be a good one to have for people.(Also… I will then be able to remember the syntax I need to show
that I really really really really really think that the way “!” works
is backwards, if the whole point of linearity is for safety of things.
I figure the syntax will never change, but I figure I should make the
argument one last time, with code.
I used to think it was on par with staring at STL compile errors in C++;
now I think it isn’t too bad (but I understand your point about a newbie
having trouble staring at it - maybe the json approach will provide a less
correct but alternative and prettier explanations/guesses).
There is some work still to be done in describing some terms in the error
messages, but here’s what we have now:
Also, Hongwei’s example and maybe others could be added to a tutorial -
here’s a simple one:
Brandon Barker
brandon…@gmail.comOn Fri, Aug 15, 2014 at 5:12 PM, Raoul Duke rao...@gmail.com wrote:
now i can only think of A Clockwork Orange…
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb5tPe23WCHiCp%3DuDCaSpRzp2Efwz_icCgpGoXxXfPiZGw%40mail.gmail.com
.
To get a clear message like “illegal: 1 + x == x” is very difficult
to do in general.
If one has some basic understanding of typechecking in ATS, then
one can often use type annotations to get more accurate/informative
messages.
When programming in ATS, one is expected to be able to tell the type
of any expression in his or her code. If not, then one may get lost even
if type-error messages are prettified.
When I program in ATS, I primarily rely on the source locations reported
by the typechecker to fix my code. Sometimes, I use showtype and
showviewtype.
Sometimes, I try to provide static/template arguments explicitly.On Friday, August 15, 2014 5:40:42 PM UTC-4, Raoul Duke wrote:
I once worked on a theorem-proving project and we spent a LOT of time
on prettifying the output of our theorem-prover. This somewhat
traumatizing
experience taught me to be wary of pretty-printing.ah, ok, good point then – actual experience!
here’s me w/out that experience, as a newbie, thinking: anything that
can be written as actual mathematical symbols (e.g. “illegal: 1 + x ==
x”) rather than as the names used internally by the solver etc. would
be better UI/UX i think.i guess i hope there’s a way to do something like that but to do it in
light of your experiences? where do you think it went off track? are
there small wins that could be attained if not for ‘solving’ the whole
question?
agreed, that was a very useful tutorial!
martinOn Wed, Aug 13, 2014 at 9:44 PM, Raoul Duke rao...@gmail.com wrote:
Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.Maybe we can even convene again some time?
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb5E9cXO%2B%2BzT7bMs_DtufKYcRKntjiN1arGdWUCqT5r%3DYA%40mail.gmail.com
.
I think if Will posts his annotated code that he worked on during the
tutorial session, that will be a good one to have for people.
(Also… I will then be able to remember the syntax I need to show
that I really really really really really think that the way “!” works
is backwards, if the whole point of linearity is for safety of things.
I figure the syntax will never change, but I figure I should make the
argument one last time, with code. 
http://julialang.org/teaching/ ← it might be nice to have something like
this, at some point soon. Not saying it is priority #1 but it could
possible be done in parallel with other teaching/meetups. Even if videos
are not the best way to get a feel for ATS as opposed to some dynamically
typed “interpreted” language, I think it would still show the human element
better, and that there’s an interested community (and that ATS isn’t just
an ivory tower gig).
Also, sorry for always referencing julialang… but it is easier to just
use one good example.
Brandon Barker
brandon…@gmail.comOn Thu, Aug 14, 2014 at 12:44 AM, Raoul Duke rao...@gmail.com wrote:
Thanks to Will for being a stupendously great, knowledgeable, patient,
helpful, and all around terrific tutor. Somebody seriously give that
gentleman a raise.Thanks for everybody who attended in person, or in spirit. Apologies
for the vagaries of the teleconferencing setup.Maybe we can even convene again some time?
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb5E9cXO%2B%2BzT7bMs_DtufKYcRKntjiN1arGdWUCqT5r%3DYA%40mail.gmail.com
.
There is no plan to change the format of the constraints.
I once worked on a theorem-proving project and we spent a LOT of time
on prettifying the output of our theorem-prover. This somewhat traumatizing
experience taught me to be wary of pretty-printing.On Friday, August 15, 2014 5:21:30 PM UTC-4, Raoul Duke wrote:
I think such a document would be far more useful than pretty-printing
constraints at this point.Is this because the format of the constraints might change? Otherwise
I cannot agree