On Mon, Oct 22, 2018 at 1:38 AM gmhwxi wrote:
>
>
> Yes, you can already use ATS2 with Z3:
>
> https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ATS-extsolve-z3
>
I wrote a bit about using it here:
https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html
--
On Mon, Oct 22, 2018 at 3:19 PM Hongwei Xi wrote:
>
> A few years back, I looked into to the possibility of using CINT
> build an REPL for ATS2. Now Cling seems to be under active development:
Can TCC compile ATS code? https://bellard.org/tcc/
It can be used as a dynamic code generator as well
On Monday, October 22, 2018 at 2:34:29 AM UTC-5, Chris Double wrote:
>
> On Mon, Oct 22, 2018 at 3:19 PM Hongwei Xi >
> wrote:
> >
> > A few years back, I looked into to the possibility of using CINT
> > build an REPL for ATS2. Now Cling seems to be under active development:
>
> Can TCC
Seems to be on of the big arguments for using Go. Of course ATS will
(rightly) never match the simplicity criteria that they strive for.
Though I imagine for more "complicated" scripts typechecking/constraint
solving may become the predominant portion of time spent among compiling
and running
so just to be a pedantic defender of real UX, please everybody note that
(at least according to me) scripting != repl, and repl does not guarantee
good ux. an actually useful, helpful, repl bestows new super powers on
those who can get their hands on such magical, enchanted, tools. it likely
This is an aside, but perhaps caching constraint solving and the like
would be a good idea? I know Agda will not re-typecheck a module
dependency unless it is touched.
On 10/22/18 4:05 PM, Brandon Barker wrote:
> Seems to be on of the big arguments for using Go. Of course ATS will
> (rightly)
Yes. Please use v0.9.26. TCC v0.9.25 is buggy and should be
avoided.
I like TCC a lot. It is a pity that it does not get maintained these days.
With TCC, I often use ATS for scripting. Once adequate lib support is
put into place, I feel that ATS can work very well for the need of shell
On Tue, Oct 23, 2018 at 10:05 AM Brandon Barker
wrote:
> Though I imagine for more "complicated" scripts typechecking/constraint
> solving may become the predominant portion of time spent among compiling and
> running code (at least in some cases). Though in this case, it probably is
> less
>>Of course ATS will (rightly) never match the simplicity criteria that
they strive for.
I won't give up so quickly :)
Go is a fine language. But Go lacks what I call "high mechanism" that can
greatly increase
one's programming productivity.
With enhanced type inference and embeddable
>>perhaps caching constraint solving and the like would be a good idea?
Definitely. Right now, patsopt typechecks the prelude files every time when
it is called.
On Mon, Oct 22, 2018 at 6:42 PM Vanessa McHale
wrote:
> This is an aside, but perhaps caching constraint solving and the like
>
10 matches
Mail list logo