runtimeverification · shd101wyy · Mar 23, 2021 · Apr 10, 2021 · Apr 10, 2021
diff --git a/Design.md b/Design.md
@@ -4,7 +4,7 @@ The design of IELE was based on our experience with formally defining [dozens of
 
 * [KEVM](https://github.com/kframework/evm-semantics), our semantics of the [Ethereum Virtual Machine](https://github.com/ethereum/yellowpaper) (EVM); and
 
-* KLLVM, our semantics of [LLVM](http://llvm.org); the latest version of the LLVM semantics will be made public when complete and published, but an earlier version [is available](https://github.com/kframework/llvm-semantics).
+* KLLVM, our semantics of [LLVM](https://llvm.org/); the latest version of the LLVM semantics will be made public when complete and published, but an earlier version [is available](https://github.com/kframework/llvm-semantics).
 
 Unlike the EVM, which is a stack-based machine, IELE is a register-based machine, like LLVM. IELE also directly supports functions, like LLVM. It has an unbounded number of registers and also supports unbounded integers. There are some tricky but manageable aspects with respect to gas calculation, a critical part of the design.
 
@@ -20,7 +20,7 @@ Here are the forces that drove the design of IELE:
 
 3. To make it easier to write secure smart contracts.  This includes writing requirements specifications that smart contracts must obey as well as making it easier to develop automated techniques that mathematically verify / prove smart contracts correct with respect to to such specifications.  For example, pushing a possibly computed number on the stack and then jumping to it regarded as an address makes verification hard, and thus security weaker, with current smart contract paradigms.  IELE has named labels, like LLVM, and jump statements can only jump to those labels.  Also, avoiding the use of a bounded stack and not having to worry about stack or arithmetic overflow makes specification and verification of smart contracts significantly easier.
 
-Like [KEVM](https://github.com/kframework/evm-semantics), the formal semantics of EVM that we previously defined, validated and evaluated using the [K framework](http://kframework.org), the design of IELE was also done in a semantics-based style, using K. Together with a fast (LLVM-based) execution backend for K that is still under development, it is expected that the interpreter obtained automatically from the semantics of IELE will be sufficiently efficient to serve as a reference implementation of IELE.
+Like [KEVM](https://github.com/kframework/evm-semantics), the formal semantics of EVM that we previously defined, validated and evaluated using the [K framework](https://kframework.org), the design of IELE was also done in a semantics-based style, using K. Together with a fast (LLVM-based) execution backend for K that is still under development, it is expected that the interpreter obtained automatically from the semantics of IELE will be sufficiently efficient to serve as a reference implementation of IELE.
 
 
 # Design Changes Relative to EVM

diff --git a/INSTALL.md b/INSTALL.md
@@ -70,7 +70,7 @@ It is safe to skip any of these dependencies that are already installed.
 Follow the instructions below.
 Perform all steps as your normal (non-root) user.
 You may find the same instructions and our public key at <https://runtimeverification.cachix.org>.
-To follow this instructions, you will need `curl` installed on your system <https://curl.haxx.se/download.html>.
+To follow this instructions, you will need `curl` installed on your system <https://curl.se/download.html>.
 
 #### Nix
 

diff --git a/web/.nvmrc b/web/.nvmrc
@@ -0,0 +1 @@
+lts/dubnium
diff --git a/web/build-html.js b/web/build-html.js
@@ -14,6 +14,7 @@ generatePagesFromMarkdownFiles({
   sourceDirectory: path.resolve(__dirname, "../"),
   outputDirectory: path.resolve(__dirname, "./public_content/"),
   websiteDirectory: path.resolve(__dirname, "./public_content/"),
+  websiteOrigin: "https://ielelang.org",
   template: pageTemplate,
   includeFileBasePath: path.resolve(__dirname, "./static_content/html/"),
 });
diff --git a/web/k-web-theme b/web/k-web-theme
diff --git a/web/package-lock.json b/web/package-lock.json
diff --git a/web/package.json b/web/package.json
@@ -4,7 +4,7 @@
   "description": "--- permalink: README.html copyright: Copyright (c) 2010-2020 Runtime Verification Team. All Rights Reserved. ---",
   "main": "index.html",
   "scripts": {
-    "build": "cd ./k-web-theme && npm install && npm run build && cd - && npm install ./k-web-theme && cp -r ./k-web-theme/public_content/* ./public_content/ && node build-html.js",
+    "build": "cd ./k-web-theme && npm install && npm run build && cd - && npm install ./k-web-theme && cp -r ./k-web-theme/public_content/. ./public_content/ && node build-html.js",
     "build-sitemap": "node sitemap/build-sitemap.js https://ielelang.org/",
     "serve": "http-server public_content"
   },

diff --git a/web/static_content/html/include/head.html b/web/static_content/html/include/head.html
@@ -10,6 +10,7 @@
 <meta name="keywords" content="runtime, verification, rv, k" />
 <meta name="author" content="IELE Semantics | Runtime Verification Inc" />
 <meta name="robots" content="index, follow" />
+<link rel="canonical" href="{{$PAGE_URL}}" />
 
 <!--favicon icon-->
 <link rel="icon" type="image/png" href="{{$ROOT}}/assets/img/favicon.ico" />

diff --git a/web/static_content/html/include/sidebar.html b/web/static_content/html/include/sidebar.html
@@ -23,8 +23,8 @@
   <nav class="collapse bd-links" aria-label="Main navigation">
     <div class="bd-toc-item">
       <a class="bd-toc-link" href="{{$ROOT}}/">Homepage</a>
-      <a class="bd-toc-link" href="{{$ROOT}}/INSTALL">Install</a>
-      <a class="bd-toc-link" href="{{$ROOT}}/Design">Design</a>
+      <a class="bd-toc-link" href="{{$ROOT}}/INSTALL/">Install</a>
+      <a class="bd-toc-link" href="{{$ROOT}}/Design/">Design</a>
     </div>
   </nav>
 </div>
+1 −0		.nvmrc
+28 −7		index.js
+0 −3		static_content/assets/sass/components/_team.scss
+9 −0		static_content/assets/vl-nav/css/core-menu.css