[Agda] Different versions of agda on Windows and Linux

[Makoto Takeyama]

Dear Anton,

> The windows version
> supports hidden arguments, whereas the linux version
> doesn't support them (it ignores any exclamation marks.

The description in the README file may be at fault.
When you build the platform independent source on Linux, please try

aclocal -I macros
autoconf
./configure --enable-newsyntax
make

(The third line is different from what's told in README)

This should make the compiled emacsagda to behave like the windows version,
i.e. as described in Sec.1.6 of Agda Tutorial.

If you are using ghc-6.6 (the latest), 'make' may stop in errors.  This is
because the source files of Agda is in ISO-8859-1 encoding while ghc-6.6
requires UTF-8 encoded files.  We are preparing a better solution, but for now
please convert problematic source files by hand, e.g.

cd Agda/src
mv Id.hs Id.tmp
iconv -f ISO-8859-1 -t UTF-8 Id.tmp > Id.hs

and similarly for Lex.hs and PreStrings.hs.
(The better solution is
http://cvs.haskell.org/trac/ghc/ticket/690
)

Best wishes,
Makoto

> 
> I have a problem with different versions of Agda under Linux and Windows
> at the moment. This is quite urgent, since tomorrow my lecture course
> on interactive theorem proving starts tomorrow, and I probably have to
> start using Agda within about a week at the latest.
> 
> At the moment the latest version of Agda (1.0.1) is only available as a
> windows installer.
> I therefore under Linux which is what I am using in my office I
> installed agda 1.0.0rc4 which seems to be the latest version which
> is available under Linux.
> In order to be consistent, I installed under windows version 1.0.0rc4
> as well, which I need at times, since sometimes in my lectures
> the data projector doesn't work under windows, and then it is
> necessary to reboot using windows.
> I wanted to test this as well, since my students will usually
> be using windows.
> 
> It turns out that the windows version 1.0.0rc4 is different
> from the linux version 1.0.0rc4: The windows version
> supports hidden arguments, whereas the linux version
> doesn't support them (it ignores any exclamation marks.
> 
> It would be nice if anybody could provide me with a platform
> independent version for one of the latest versions, which
> conincides with the windows version, preferably with the latest
> one, even if it is not made available on the sourceforge
> web site.
> 
> Please help me to keep my course running,
> 
> Thanks a lot,
> 
> Anton
> 
> -- 
> ---------------------------------------
> Anton Setzer
> Department of Computer Science
> University of Wales Swansea
> Singleton Park
> Swansea SA2 8PP
> UK
> 
> Telephone:
> (national)        (01792) 513368
> (international) +44 1792  513368
> Fax:
> (national)        (01792) 295708
> (international) +44 1792  295708
> Visiting address:
> Faraday Building,
> Computer Science Dept.
> 2nd floor, room 211.
> Email: a.g.setzer at swan.ac.uk
> WWW:
> http://www.cs.swan.ac.uk/~csetzer/
> ---------------------------------------
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Makoto Takeyama
AIST/CVS (National Institute of Advanced Industrial Science and Technology /
          Research Center for Verification and Semantics)
tel: +81-6-4863-5019   fax: +81-6-4863-5052