[Logiweb] Transitively referenced pages

[Klaus Ebbe Grue]

Hi Frederik,

You describe a situation with the following references:
   B -> A
   C -> B
   C -> A
Then you update A to A2 and C to C2, which creates
   B -> A
   C2 -> B
   C2 -> A2
That gives problems because lemmas in B reference constructs in A whereas 
lemmas in C2 reference constructs in A2. That essentially makes lemmas in 
B useless in C2.

There is no counter to this problem except recompiling B after 
recompiling A and before recompiling C. Sorry. And there is basically no 
way to change the situation.

The problem a consequence of the immutability of Logiweb pages. It is much 
like the problem in functional programming that if one wants to change the 
last element of a list, then one has to reconstruct the entire list. 
Immutability has its drawbacks, but Logiweb depends completely on it. 
Without immutability, there would be worse problems.

My suggestion until further is one of
1) recompile B manually whenever A is recompiled.
2) set up make files for recompiling referenced pages when .lgw
    is older than .pyk.
3) work on one big page.

Option 3) is obviously a bad choice if the page is very big. I suggest 
(I suppose you already do this, so it is not much of a help) that you put 
very stable things in page A so you rarely need to recompile A, that you 
put less stable things in B so you occasionally need to recompile B and 
that you put you experimental proofs in C. I have never bothered to set 
up make files myself.

If possible, run Logiweb on a fast machine of your own. Diku's computers 
are often saturated, and a standard gaming computer with dual boot and
Linux/Logiweb works fine for me.

Klaus
-------------- next part --------------
_______________________________________________
Logiweb mailing list
Logiweb at diku.dk
http://lists.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)