Cross-compilation is in decent shape even with ATS2, at least on Debian.
I can cross-compile a program for Raspberry Pi using Debian-provided
cross-compilers.
I have built binaries for many platforms you can imagine, including
Redox https://github.com/vmchale/illiterate/releases
As for package
Dear Hongwei,
Thanks for your great effort for developing ATS3.
I can hardly wait publishing your first release of ATS3 manual!
On Sat, Oct 20, 2018 at 10:48 AM gmhwxi wrote:
> I currently have no plan to add more support for theorem-proving in ATS3.
OK. It's just idea. No problem.
> My
Hi Kiwamu,
As always, thanks for your input!
I currently have no plan to add more support for theorem-proving in ATS3.
My expectation is to find ways to make direct use of existing
theorem-proving
systems (e.g., Isabel, Coq, Lean, various SMT solvers, etc.).
I certainly want to be ambitious
Ah -- I was referring to atscc2js / atscc2php / atscc2py3, etc, not the
built-in *codegen2 *feature (sorry if I was ambiguous). If one compiles to
separate files in say, PHP, then some of the functions that are normally
static or inlined in C (eg, __patsfun_*) may have duplicate names, causing
Here is one way of using codegens that I perceive:
Use codegens to generate code and the generated code is
stored in a file, say, of the name xyz.hats. Then one can do
local
#include xyz.hats
in
[Some code that needs the content of xyz.hats]
end
The generated code often contains a lot of
Thanks for the responses.
Along with the gcc optimizations, code generated in a single file (with
`patsopt -dd` or `mylibies_link.hats`) tends to play more nicely with
codegens, which may or may not have a notion of a "static" function like in
C (making namespace collisions possible with
