This directory produces a peculiar issue when the file UntypedLambda.agda is loaded, as per this message on the Agda mailing list: Hi folks First, thanks for the aquamacs tips. Whatever it was, it's now in colour and going well. (Peculiarly, before I copied .emacs stuff from Ulf, I had *one* file which suddenly started appearing in colour for no obvious reason, when the rest stayed stubbornly monochrome. Hmm.) So yes, I've been messing about with enough stuff to need more than one file. And I've hit a distinctly bizarre happening. Maybe I'm not using modules in the right way, but I don't think it's falling over as gracefully as it might. I know these things take time, and I expect I can work around the issue. Er, um, I'm afraid I've (tried and) failed to condense the problem to a toy example, so I'll summarize. If you want a tar of the files, just ask. Here goes. I developed a library of stuff in short files, not entirely linearly. I wanted to build a wrapper so I could import in one go. {--- begin Syntacticosmos.agda ----------------------} module Syntacticosmos (Gnd : Set)(U : Set)(El : U -> Set) where open import Basics open import Pr open import Nom import Kind open module KindGUEl = Kind Gnd U El public import Cxt open module CxtK = Cxt Kind public import Loc open module LocK = Loc Kind public import Term open module TermGUEl = Term Gnd U El public import Shift open module ShiftGUEl = Shift Gnd U El public import Eta open module EtaGUEl = Eta Gnd U El public import Inst open module InstGUEl = Inst Gnd U El public import Subst open module SubstGUEl = Subst Gnd U El public {--- end Syntacticosmos.agda ----------------------} The file loads fine. So far so good. Then I tried to use it... {--- begin UntypedLambda.agda -----------------------} module UntypedLambda where open import Basics open import Pr open import Nom import Syntacticosmos data Tag : Set where lamT : Tag appT : Tag open module ULam = Syntacticosmos TT TT (\_ -> Tag) LAM : Kind LAM = Ty _ SigLAM : Kind SigLAM = Pi _ conk where conk : Tag -> Kind conk lamT = (LAM |> LAM) |> LAM conk appT = LAM |> LAM |> LAM Lam : Cxt -> Set Lam G = G [! SigLAM !]- LAM lam : {G : Cxt}(x : Nom){Gx : [| G Hasn't x |]} -> Lam ((G [ x - LAM ]) {Gx}) -> Lam G lam x {Gx} b = G[ lamT G^ G\\ (bind x {Gx} b) G& Gnil ] app : {G : Cxt} -> Lam G -> Lam G -> Lam G app f s = G[ appT G^ f G& s G& Gnil ] moo : Lam EC moo = lam Ze (lam (Su Ze) (var Ze)) noo : Lam EC noo = lam (Su Ze) (lam Ze (var (Su Ze))) coo : Id moo noo coo = refl {--- end UntypedLambda.agda ----------------------------} When I try to load UntypedLambda.agda, it fails at import Syntacticosmos with the following error: /Users/ctm/Desktop/Syntacticosmos/UntypedLambda.agda:6,1-22 /Users/ctm/Desktop/Syntacticosmos/Syntacticosmos.agdai: getModificationTime: does not exist (No such file or directory) Moreover, by the joy of Finder, I watched the directory as this ran. The file Syntacticosmos.agdai appeared and then disappeared in the course of the failed load. My attempts to mimic the pattern of files with similar structure but less distraction have not reproduced the problem. I hope you enjoy the distraction... Does this ring any bells with any one? How should I be organizing the library modules, anyway? I'm sorry it's all a bit sick. On the upside, I'm really pleased at the way the engines are taking what I'm throwing at them (a universe of globally named, locally nameless syntaxes with binding). I probably shouldn't be allowed this much fun, but it's the weekend and I'm not so well at the moment, hence hacking therapy. Anyhow, I thought I'd share this peculiar happening. I don't even know how to begin speculating about the problem. All the best Conor _______________________________________________ Agda mailing list Agda@lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda