-
Notifications
You must be signed in to change notification settings - Fork 42
/
updatehtml
executable file
·106 lines (93 loc) · 5.1 KB
/
updatehtml
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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
#!/bin/bash
# run from ~/TypeTopology/source
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 -f ~/martinescardo.github.io/TypeTopology/*.html # do not delete Agda.css, as it is a modified version
mv html/*.html ~/martinescardo.github.io/TypeTopology/
cd ~/martinescardo.github.io/
# Now create copies for files that have been moved to other places
# but are linked from published papers, blogs etc.
# Symbolic links don't work any more, so we replace "ln -s" by "cp -a"
# Deprecated - agda-new should not be offered as a public link any more,
# for some years now:
cp -a TypeTopology agda-new
chmod a+r agda-new/*.html
git add agda-new
cd ~/martinescardo.github.io/TypeTopology/
cp -a CantorSchroederBernstein.CSB.html CantorSchroederBernstein.html
cp -a CoNaturals.GenericConvergentSequence.html GenericConvergentSequence.html
cp -a DomainTheory.ScottModelOfPCF.ScottModelOfPCF.html PCFModules.html
cp -a Factorial.Law.html UF-Factorial.html
cp -a Fin.ArithmeticViaEquivalence.html ArithmeticViaEquivalence.html
cp -a Fin.index.html Fin-Properties.html
cp -a Fin.Type.html Fin.html
cp -a Fin.UniverseInvariance.html UF-Finiteness-Universe-Invariance.html
cp -a Games.FiniteHistoryDependent.html FiniteHistoryDependentGames.html
cp -a Groups.Free.html FreeGroup.html
cp -a Groups.Free.html FreeGroupOfLargeLocallySmallSet.html
cp -a Locales.AdjointFunctorTheoremForFrames.html AdjointFunctorTheoremForFrames.html
cp -a Locales.CompactRegular.html CompactRegular.html
cp -a Locales.Frame.html Frame.html
cp -a Locales.GaloisConnection.html GaloisConnection.html
cp -a Locales.HeytingImplication.html HeytingImplication.html
cp -a NotionsOfDecidability.SemiDecidable.html SemiDecidable.html
cp -a Ordinals.AdditionProperties.html OrdinalArithmetic-Properties.html
cp -a Ordinals.BuraliForti.html BuraliForti.html
cp -a Ordinals.Notions.html Ordinal-Notions.html
cp -a Ordinals.OrdinalOfOrdinals.html OrdinalOfOrdinals.html
cp -a Ordinals.WellOrderTransport.html OrdinalsWellOrderTransport.html
cp -a Ordinals.index.html Ordinals.html
cp -a Various.Types2019.html Types2019.html
cp -a Slice.Construction.html Slice.html
cp -a TypeTopology.ADecidableQuantificationOverTheNaturals.html ADecidableQuantificationOverTheNaturals.html
cp -a UF.DiscreteAndSeparated.html DiscreteAndSeparated.html
cp -a TypeTopology.GenericConvergentSequenceCompactness.html ConvergentSequenceCompactness.html
cp -a UF.Choice.html UF-Choice.html
cp -a UF.Size.html UF-Size.html
cp -a UF.UniverseEmbedding.html UniverseEmbedding.html
cp -a UF.Yoneda.html UF-Yoneda.html
cp -a UF.index.html UF.html
cp -a UF.HiggsInvolutionTheorem.html Various.HiggsInvolutionTheorem.html
cp -a Various.Dedekind.html Dedekind.html
cp -a Various.HiggsInvolutionTheorem.html HiggsInvolutionTheorem.html
cp -a Various.LawvereFPT.html LawvereFPT.html
cp -a Various.UnivalenceFromScratch.html UnivalenceFromScratch.html
# From now on (12th Jan 2023), published things should go to
# ~/martinescardo.github.io/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.
cp -a DomainTheory.index.html Published.DomainTheory.index.html
cp -a DomainTheory.Bilimits.Dinfinity.html Published.DomainTheory.Bilimits.Dinfinity.html
cp -a DomainTheory.ScottModelOfPCF.ScottModelOfPCF.html Published.DomainTheory.ScottModelOfPCF.ScottModelOfPCF.html
cp -a Lifting.IdentityViaSIP.html Published.Lifting.IdentityViaSIP.html
cp -a NotionsOfDecidability.SemiDecidable.html Published.NotionsOfDecidability.SemiDecidable.html
cp -a Slice.Construction.html Published.Slice.Slice.html
cp -a Ordinals.BuraliForti.html Published.Ordinals.BuraliForti.html
cp -a Ordinals.OrdinalOfOrdinals.html Published.Ordinals.OrdinalOfOrdinals.html
cp -a Ordinals.OrdinalOfOrdinalsSuprema.html Published.Ordinals.OrdinalOfOrdinalsSuprema.html
cp -a Ordinals.Type.html Published.Ordinals.Type.html
cp -a TypeTopology.CompactTypes.html Published.TypeTopology.CompactTypes.html
cp -a TypeTopology.Density.html Published.TypeTopology.Density.html
cp -a UF.DiscreteAndSeparated.html Published.TypeTopology.DiscreteAndSeparated.html
cp -a TypeTopology.SimpleTypes.html Published.TypeTopology.SimpleTypes.html
cp -a Quotient.Large-Variation.html Published.UF.Quotient-F.html
cp -a Quotient.index.html Published.UF.Quotient.html
cp -a Quotient.index.html Published.UF.Quotient-Replacement.html
cp -a Quotient.Large.html Published.UF.Large-Quotient.html
cp -a Various.Dedekind.html Published.Various.Dedekind.html
# Further links using the Published.* scheme
# Added by Tom de Jong - 31 March 2023, 18 April 2023
cp -a UF.Size.html Published.UF.Size.html
cp -a UF.ImageAndSurjection.html Published.UF.ImageAndSurjection.html
# Added by Tom de Jong on 3 October 2023.
cp -a PCF.Lambda.index.html Published.PCF.Lambda.index.html
# git add the above files
cd ..
chmod a+r TypeTopology/*
git add TypeTopology