Re: contrib version 0.2.10 vs 0.2.12
Le mardi 6 décembre 2016 17:47:16 UTC+1, gmhwxi a écrit : > > Yes. The issue should be fixed in the next release. > > The reason for the problem is that I myself rarely do 'make install' on my > own computer when building ATS. So I forgot the need to change the version > number in > configure.ac. I will be using a VM to do 'make install' before each > release from this point on. > As the topic is about installing, here is a variation of C9-ATS2-install.sh: https://gist.github.com/Hibou57/9077632c31c7c5af4c6e6a81f4cbc04b -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/a04c8b93-4439-40eb-a764-eb2cd4356af0%40googlegroups.com.
Re: ATS Tutorials
I guess substituting HTTP for HTTPS in the tutorial URL may solve the issue. Le vendredi 5 août 2016 21:33:14 UTC+2, Steinway Wu a écrit : > > Sadly, there is a https related issue. I hope to fix it soon... for now, > it works with Safari at least. I'm not particularly familiar of how to work > with http requests in a https served pages. Any one has any idea? Please > let me know. Thanks. > > UPDATE: > > Ok, in Chrome, you need to head over to http*s*://www.ats-lang.org/ > first, when Chrome warns about certificate mismatch, choose to proceed > anyway, dismissing the warning. Then Chrome will remember your choice, and > the tutorial website will work again. > > On Friday, August 5, 2016 at 3:12:42 PM UTC-4, Steinway Wu wrote: >> >> Hi, >> >> Following up on Hongwei's *ats-as-a-service*, I wrote a pandoc plugin >> for automating some of the tasks of writing interactive ats tutorials, >> shown here https://steinwaywhw.github.io/ats-tutorials/. If you a >> familiar with pandoc, then my small script is just a pandoc filter in >> python, that takes in a code block in original markdown input, and turn it >> into interactive or just highlighted html snippets. >> >> The project home page https://steinwaywhw.github.io/ats-tutorials/ >> itself is rendered using this plug-in. Hope it is useful for anyone who >> want to write code-related webpages. Contributions are welcomed. The tool >> is MIT licensed. >> > -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/6e1fa209-53ac-43b6-b319-e48d8987755b%40googlegroups.com.
Re: [ats-lang-users] ATS2-0.2.12 released
Le vendredi 2 décembre 2016 21:25:06 UTC+1, gmhwxi a écrit : > > > I think I have fixed the issue. Please delete ATS2-contrib and > try again. > Indeed, it works now (with Contrib from trunk). Just that the ATS version looks like it is still 0.2.10 instead of 0.2.12. Talking about Contrib, I wondered if the one from GitHub and the one from SourceForge could get different names, as they are not interchangeable. The one from GitHub is OK to compile ATS but not the one from SourceForge, so may be a name like Contrib-Build-Dep for the one from GitHub. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/275ffa6f-6674-4d8b-bacf-94099ad6ec37%40googlegroups.com.
Re: [ats-lang-users] ATS2-0.2.12 released
Installing the updated version using `C9-ATS2-install.sh`, I got this error: cat: output/DATS/ML/list0_dats.php: Aucun fichier ou dossier de ce type cat: output/DATS/ML/array0_dats.php: Aucun fichier ou dossier de ce type « Aucun fichier ou dossier de ce type » means “No such file or directory”. I will disable the PHP target, as I was to do something mainly with the JavaScript target. Le jeudi 24 novembre 2016 17:00:36 UTC+1, gmhwxi a écrit : > > > -- Forwarded message -- > > Hi, > > I am pleased to announce the release of ATS2-0.2.12. > […] > -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/60bf49e9-57b9-406b-a638-8d07972cdd34%40googlegroups.com.
Re: [ats-lang-users] ATS2-0.2.12 released
Le mardi 6 décembre 2016 03:54:26 UTC+1, gmhwxi a écrit : > > > > If you could tell me how this happened, I would like to fix it. Thanks! > > Oops, sorry, I should have tell more. That's the subdirectory in lib, which is named `ats2-postiats-0.2.10` and the wrapper scripts in `bin` which says `PACKAGE_VERSION=0.2.10`. It is so, using the `C9-ATS2-install.sh` script. I remember the same already occurred in the past. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/6c561fe8-b74c-4514-8f2f-98f8dc4a52ac%40googlegroups.com.
Re: contrib version 0.2.10 vs 0.2.12
If they are people using it, please, update it. I made an important change since I mentioned it here. It's about a git command (among other smaller things). I just remember to tell for some reason just now, I forget to tell earlier. With my apologies … Le jeudi 8 décembre 2016 15:49:49 UTC+1, gmhwxi a écrit : > > Thanks! > > It is now mentioned on the ATS Download/SCRIPT page: > > https://github.com/ats-lang/ats-lang.github.io/tree/master/SCRIPT > >> >> -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/94532ad2-3067-4f55-8152-ddce644ba05a%40googlegroups.com.
Re: Meaning of `#[…]`
Le mercredi 1 août 2018 17:08:17 UTC+2, Artyom Shalkhakov a écrit : > > Hi Steinway, > > Thanks for your input! > > I think Yannick is very good at posing interesting questions. :-) > Documenting ATS2, deserves questionning :-D -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/a7d8c187-7abb-45fd-a3ca-514d546aee6d%40googlegroups.com.
Re: Cross-compiling for Windows
Seems you are not the first one to face this issue : https://github.com/gotk3/gotk3/issues/204 As Artyom said, it is POSIX related : http://pubs.opengroup.org/onlinepubs/7908799/xsh/systypes.h.html As an example, it appears in a struct for password entry : http://pubs.opengroup.org/onlinepubs/7908799/xsh/pwd.h.html I would be surprised this is really required to compile Postiats … must be an error or else I don’t see why it would be needed. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/8f270c6f-6942-485a-9d9c-13a4cc989239%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le vendredi 3 août 2018 22:18:48 UTC+2, Yannick Duchêne a écrit : > > > > Le vendredi 3 août 2018 22:17:24 UTC+2, Yannick Duchêne a écrit : >> >> >> So `view@` peaks something? >> >> > Oops, I wanted ti say “peek” instead of “peak” > Yes, I’m silly: view@ is subject to linear logic. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/26eaceed-b37b-46cd-b38b-f1180c90b383%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le vendredi 3 août 2018 22:11:51 UTC+2, gmhwxi a écrit : > > > It will be okay if you put 'p' back: > > // `g` evaluates `f` and then frees it. > fn g(f: >> t?): int = let > val r = f() > val _ = cloptr_free($UN.castvwtp0(f)) > prval p = view@ f // <-- here > prval () =view@f := p > in r end > > So `view@` peaks something? The `view@f := p` is what is called “view restauration”, isn’t it? That’s something I not yet investigated. > >>val _ = cloptr_free($UN.castvwtp0(f)) > > The above line is safe. We just need to find a better way to name it :) > What about just moving it out of `unsafe.sats` I did not knew it is safe, I will have a new look at it. Thanks for the point. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/1ffee64c-fcfa-473c-98cd-a2d28b60c8d0%40googlegroups.com.
Re: Effects of proofs on types as a side effect
Le samedi 4 août 2018 16:43:28 UTC+2, gmhwxi a écrit : > > Here is what I have in mind at this moment: > > ATS3 = ATS2 + meta-programming > > Type inference plays a big role to provide support for meta-programming. > That’s fine :) -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/69e57240-73a1-430f-903b-0a4baba6dde6%40googlegroups.com.
Re: <> in first part of function return type
Le samedi 4 août 2018 16:38:00 UTC+2, gmhwxi a écrit : > > […] > >>var h:t = lam@() => ()// <-- here > > 'var h:t' means that the size of 'h' is that of the size of 't'. > It does NOT mean that only a value of the type 't' can be > stored in 'h'. > Indeed, if I do what’s below, the function effect must be set to pure: typedef t = () - void var h = (lam@() =<0> ()):t I was not suspecting this, because when a mention to “master type” was made some times ago, I though the typing rules for initialisation, was like with `val`, and I added this a long time ago in my notes, about `val`: > `val x = e:T`: typical of annotations, checks `e` is of type `T`. > `val x:T = e`: checks `e` is of a subtype of `T`. So I was surprised about `var h:t = lam@() => ()` However, although it triggers another error, for type checking, with what is below, the function effect is required to be pure: val h:t = lam@() =<0> () // For a test only, otherwise requires to be an l‑value. Values and variables differ more than I suspected. I will need a deeper look at it and to review every thing with this question in mind. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/90d7e98a-f2a4-49c9-8005-3b0ec60688c3%40googlegroups.com.
Postiats and C errors with array
I’m unsure if it’s something wrong with what I wrote (ex. may be it’s not allowed) or with Postiats. The sample below type‑checks, but compilation fails with an INTERROR message. The sample: typedef row = @[int][3] val row1:row = @[int](1, 2, 3) val row2:row = @[int](4, 5, 6) var a = @[row][2](row1, row2) val a12 = a[1].[2] On the second line, it fails with: > INTERROR(pats_ccomp_dynexp): hidexp_ccomp: hde0 = HDEarrinit(HSEapp(HSEcst(atstkind_t0ype); HSEs2exp(S2Eextkind(atstype_int))); HDEint(3); HDEi0nt(1); HDEi0nt(2); HDEi0nt(3)) If I try this instead: typedef row = @[int][3] var row1:row = @[int](1, 2, 3) var row2:row = @[int](4, 5, 6) var a = @[row][2](row1, row2) val a12 = a[1].[2] … Postiats can compile it, but I then I have numerous error while compiling C. Many of these errors mentions ATSstatmpdec and there are also C syntax errors. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9695cba1-b5c0-463e-9356-60035b1bb142%40googlegroups.com.
Effects of proofs on types as a side effect
Here is sample, what’s important is in `g` marked `<-- here`: staload UN = "prelude/SATS/unsafe.sats" // Prerequisite. viewtypedef t = () - int // Prerequisite. fn h(): t = let val v = 1 in lam(): int => v end // `g` evaluates `f` and then frees it. fn g(f: >> t?): int = let val r = f() val _ = cloptr_free($UN.castvwtp0(f)) prval p = view@ f // <-- here in r end var f = h() val v = g(f) The presence of `prval p = view@ f` produce a type error in `in r end`, which is not about `r`, rather about `>> t?` which is treated as something returned too. I’m surprised this proof which does not go outside the function, can change the returned type of `f`. I encountered other similar effects, including one without proof, this one is the simplest one. For the anecdote, I came to this while testing if there are ways to free the cloptr without an unsafe cast. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/acad14e7-3f3b-4daf-9105-78864b00034a%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 03:37:55 UTC+2, Julian Fondren a écrit : > > Incidentally, this works: > > #include "share/atspre_staload.hats" > > typedef row = @(int, int, int) > val row1: row = (1, 2, 3) > val row2: row = (4, 5, 6) > var a = @[row](row1, row2) > val a12 = a[1].2 > > implement main0() = println!(a12) > > > So with tuples. Indeed, I know it works, but I was trying some samples to document expressions of the form `[…] ` and wanted to try second level indexing of arrays. By the way, I wonder why `#include "share/atspre_staload.hats"` of the basics which are always loaded by default, because "share/atspre_staload.hats" seems often required. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/e3fb18b9-b344-4be2-8b53-10dc1ea2edf0%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 21:40:16 UTC+2, gmhwxi a écrit : > > >>Python surprisingly does not have direct support for arrays, > > Python is not famous for being effcient :) > I know, at least 40x worse than the equivalent in any imperative language. I’m using it rather for its terse syntax (and because it’s everywhere), but I badly miss typing with it (PyLint helps a bit to workaround this, but just a bit). Talking about it, the first thing I will do when the documentation I attempt to write will be finished, is to try to port my Postiats utilities to ATS2 and see how much I can have something as terse as the Python version. I believe it will be a good real world exercice (for know, I just tested ATS2 with propositions based proving three years ago, and I gave up, because I wanted too much from it). -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/a34d4710-84b5-42ab-971e-f4d6f4953952%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 10:04:58 UTC+2, Yannick Duchêne a écrit : > > […] It was not my matter, but may be for arrays with multiple dimension, > using abstract types and external implementation may be an option, but I > have never tried it. > Or rather interpret one-dimension array as the storage of a multi‑dimensions array. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/4939d5e6-d15c-433e-9d40-98b6cf917c45%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 04:18:01 UTC+2, gmhwxi a écrit : > > > @[int][3] is the type for a flat int array of size 3. > > Unfortunately, it is not fully supported at this point > (it can only be assigned to a var). Please use @(int, int, int) > instead. > Indeed, this works if there are only top‑level vars: #include "share/atspre_staload.hats" typedef row = @[int][3] var row:row = @[int](1, 2, 3) val r2 = row[2] I just though although multiple dimension array types is not supported, it could be supported indirectly the way I tried it. It was not my matter, but may be for arrays with multiple dimension, using abstract types and external implementation may be an option, but I have never tried it. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/a35ec12f-c8f0-4871-9ac6-b588c1873885%40googlegroups.com.
Re: Postiats and C errors with array
Le mardi 7 août 2018 10:00:51 UTC+2, Yannick Duchêne a écrit : > > […] > By the way, I wonder why `#include "share/atspre_staload.hats"` of the > basics which are always loaded by default, because > "share/atspre_staload.hats" seems often required. > Typo, sorry. I wanted to say “I wonder why `#include "share/atspre_staload.hats"` **is not part** of the basics”. -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/dbbc1438-2cc8-4bde-b54a-ab806ff51e1b%40googlegroups.com.
Re: proofs vs statics?
Yes, indeed, there are proof functions and proof values (as result of proof functions) ; the word “proof” used alone is typically to mean proof function (I was unclear). Le samedi 23 mars 2019 22:35:51 UTC+1, gmhwxi a écrit : > > No, a proof is not a type. A proof is a total program (that is pure and > terminating). > > On Friday, March 22, 2019 at 1:55:17 PM UTC-4, Yannick Duchêne wrote: >> >> Within ATS, is it correct to say a proof is usually a dependant type? >> (whose value just get discarded from the generated program). >> >> >> P.S. Just wanted to have a quick look at some interesting talk here. >> Unfortunately, I still don’t have time to get back at ATS. >> > -- 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-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b55b4963-eb49-48b1-8652-c6e208ccf848%40googlegroups.com.
