forked from martinescardo/TypeTopology
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathupdateurl
executable file
·92 lines (82 loc) · 4.75 KB
/
updateurl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
#!/bin/bash
set -euxo pipefail
# Generate html files and deploy them.
# This is to be run from TypeTopology/source.
# It assumes that we want to deploy the html pages at ~/public_html.
rm -rf html
agda --highlight-occurrences --html AllModulesIndex.lagda
rm ~/public_html/TypeTopology/*.html # do not delete Agda.css, as it is a modified version
mv html/*.html ~/public_html/TypeTopology/
chmod a+r ~/public_html/TypeTopology/*.html
# Now create symlinks for files that have been moved to other places
# but are linked from published papers, blogs etc.
cd ~/public_html/TypeTopology/
ln -s CantorSchroederBernstein.CSB.html CantorSchroederBernstein.html
ln -s CoNaturals.GenericConvergentSequence.html GenericConvergentSequence.html
ln -s DomainTheory.ScottModelOfPCF.ScottModelOfPCF.html PCFModules.html
ln -s Factorial.Law.html UF-Factorial.html
ln -s Fin.ArithmeticViaEquivalence.html ArithmeticViaEquivalence.html
ln -s Fin.index.html Fin-Properties.html
ln -s Fin.Type.html Fin.html
ln -s Fin.UniverseInvariance.html UF-Finiteness-Universe-Invariance.html
ln -s Games.FiniteHistoryDependent.html FiniteHistoryDependentGames.html
ln -s Groups.Free.html FreeGroup.html
ln -s Groups.FreeOverLargeLocallySmallSet.html FreeGroupOfLargeLocallySmallSet.html
ln -s Locales.AdjointFunctorTheoremForFrames.html AdjointFunctorTheoremForFrames.html
ln -s Locales.CompactRegular.html CompactRegular.html
ln -s Locales.Frame.html Frame.html
ln -s Locales.GaloisConnection.html GaloisConnection.html
ln -s Locales.HeytingImplication.html HeytingImplication.html
ln -s NotionsOfDecidability.SemiDecidable.html SemiDecidable.html
ln -s Ordinals.ArithmeticProperties.html OrdinalArithmetic-Properties.html
ln -s Ordinals.BuraliForti.html BuraliForti.html
ln -s Ordinals.Notions.html Ordinal-Notions.html
ln -s Ordinals.OrdinalOfOrdinals.html OrdinalOfOrdinals.html
ln -s Ordinals.WellOrderTransport.html OrdinalsWellOrderTransport.html
ln -s Ordinals.index.html Ordinals.html
ln -s Various.Types2019.html Types2019.html
ln -s Slice.Slice.html Slice.html
ln -s TypeTopology.ADecidableQuantificationOverTheNaturals.html ADecidableQuantificationOverTheNaturals.html
ln -s TypeTopology.DiscreteAndSeparated.html DiscreteAndSeparated.html
ln -s TypeTopology.GenericConvergentSequenceCompactness.html ConvergentSequenceCompac.html
ln -s UF.Choice.html UF-Choice.html
ln -s UF.Size.html UF-Size.html
ln -s UF.UniverseEmbedding.html UniverseEmbedding.html
ln -s UF.Yoneda.html UF-Yoneda.html
ln -s UF.index.html UF.html
ln -s UF.HiggsInvolutionTheorem.html Various.HiggsInvolutionTheorem.html
ln -s Various.Dedekind.html Dedekind.html
ln -s Various.HiggsInvolutionTheorem.html HiggsInvolutionTheorem.html
ln -s Various.LawvereFPT.html LawvereFPT.html
ln -s Various.UnivalenceFromScratch.html UnivalenceFromScratch.html
# From now on (12th Jan 2023), published things should go to
# ~/public_html/TypeTopology/Published.* Use symlinks as above to
# create them. NB. Don't use subdirectories because the links in the
# symlinked html files may break.
# These are linked to in Tom de Jong's PhD thesis (2022) and duplicates some of
# the above for consistency.
ln -s DomainTheory.index.html Published.DomainTheory.index.html
ln -s DomainTheory.Bilimits.Dinfinity.html Published.DomainTheory.Bilimits.Dinfinity.html
ln -s DomainTheory.ScottModelOfPCF.ScottModelOfPCF.html Published.DomainTheory.ScottModelOfPCF.ScottModelOfPCF.html
ln -s Lifting.IdentityViaSIP.html Published.Lifting.IdentityViaSIP.html
ln -s NotionsOfDecidability.SemiDecidable.html Published.NotionsOfDecidability.SemiDecidable.html
ln -s Slice.Slice.html Published.Slice.Slice.html
ln -s Ordinals.BuraliForti.html Published.Ordinals.BuraliForti.html
ln -s Ordinals.OrdinalOfOrdinals.html Published.Ordinals.OrdinalOfOrdinals.html
ln -s Ordinals.OrdinalOfOrdinalsSuprema.html Published.Ordinals.OrdinalOfOrdinalsSuprema.html
ln -s Ordinals.Type.html Published.Ordinals.Type.html
ln -s TypeTopology.CompactTypes.html Published.TypeTopology.CompactTypes.html
ln -s TypeTopology.Density.html Published.TypeTopology.Density.html
ln -s TypeTopology.DiscreteAndSeparated.html Published.TypeTopology.DiscreteAndSeparated.html
ln -s TypeTopology.SimpleTypes.html Published.TypeTopology.SimpleTypes.html
ln -s Quotient.Large-Variation.html Published.UF.Quotient-F.html
ln -s Quotient.index.html Published.UF.Quotient.html
ln -s Quotient.index.html Published.UF.Quotient-Replacement.html
ln -s Quotient.Large.html Published.UF.Large-Quotient.html
ln -s Various.Dedekind.html Published.Various.Dedekind.html
# Further links using the Published.* scheme
# Added by Tom de Jong - 31 March 2023, 18 April 2023
ln -s UF.Size.html Published.UF.Size.html
ln -s UF.ImageAndSurjection.html Published.UF.ImageAndSurjection.html
# Added by Tom de Jong on 3 October 2023.
ln -s PCF.Lambda.index.html Published.PCF.Lambda.index.html