UlfNorell
commented
10 years ago From nils.anders.danielsson on December 10, 2013 06:13:19
Q: Are agdai files platform-independent?
From the documentation of Data.Binary (which we use):
Values encoded using the Binary class are always encoded in network order (big endian) form, and encoded data should be portable across machine endianness, word size, or compiler version. For example, data encoded using the Binary class could be written on any machine, and read back on any another.
Another issue to consider is whether we could get into trouble if we build the .agdai file using one version of binary, and some user builds Agda with another version. I guess that we're safe (modulo bugs) as long as we stick to a single, major version of binary. Currently we support two major versions.
If we start to use hashes, then we have several issues to consider:
- Newline conversion. This issue can be avoided by reading the files in binary mode (all we need is the raw UTF-8 byte stream).
- Is the hash computation platform-independent?
- Does the hash computation depend on the version of the hashing library that we use (if any)?
From andreas....@gmail.com on December 10, 2013 13:50:01
Problem 1: Primitive.agda might be installed in a location where the user has no rights to write. Thus, Primitive.agdai might not be creatable and nothing will work (at least not properly).
Problem 2 (related): Every time you cabal install, Primitive.agda is recreated in $HOME/.cabal/lib/prim/Agda/. This leads to recompilation of whole std-lib.
Proposed solution:
Implementation sketch:
Q: Are agdai files platform-independent?
Original issue: http://code.google.com/p/agda/issues/detail?id=993