rewrite URLs to drop /developer/docs

.env.example

@@ -1,4 +1,4 @@
-NEXT_PUBLIC_BASE_PATH=/developers/docs
+NEXT_PUBLIC_BASE_PATH=/
 NEXT_PUBLIC_DOCSEARCH_APP_ID=R2IYF7ETH7
 NEXT_PUBLIC_DOCSEARCH_API_KEY=599cec31baffa4868cae4e79f180729b
 NEXT_PUBLIC_DOCSEARCH_INDEX_NAME=docsearch

README.md

@@ -1,6 +1,6 @@
 # Tezos Documentation Portal (Beta)
 
-This is the source code for the Tezos Documentation Portal: https://tezos.com/developers/docs
+This is the source code for the Tezos Documentation Portal: https://docs.tezos.com
 
 ## Contributing
 

src/pages/advanced-topics/formal-verification/coq/index.md

@@ -75,10 +75,10 @@ For a more technical understanding of the operation of Mi-Cho-Coq, this tutorial
 
 We can execute the proof of 'Example test_orb2" (Example keyword below) using the Coq proof assistant.
 
-{% figure src="/developers/docs/images/coq/proof_1.jpeg" alt="coq-proof-execution-1" caption="Proof of execution with the Coq software, proving that `false or false => false`. 1/3" %}  {% /figure %}
+{% figure src="/images/coq/proof_1.jpeg" alt="coq-proof-execution-1" caption="Proof of execution with the Coq software, proving that `false or false => false`. 1/3" %}  {% /figure %}
 
-{% figure src="/developers/docs/images/coq/proof_2.jpeg" alt="coq-proof-execution-2" caption="Proof of execution with the Coq software, simplification step using the definition of `orb`. 2/3" %} {% /figure %}
+{% figure src="/images/coq/proof_2.jpeg" alt="coq-proof-execution-2" caption="Proof of execution with the Coq software, simplification step using the definition of `orb`. 2/3" %} {% /figure %}
 
-{% figure src="/developers/docs/images/coq/proof_3.jpeg" alt="coq-proof-execution-3" caption="Proof of execution with the Coq software, reflexivity step compares both terms to end the proof. 3/3" %} {% /figure %}
+{% figure src="/images/coq/proof_3.jpeg" alt="coq-proof-execution-3" caption="Proof of execution with the Coq software, reflexivity step compares both terms to end the proof. 3/3" %} {% /figure %}
 
 End of proof.

src/pages/advanced-topics/formal-verification/formal-verification-on-tezos/index.md

@@ -7,7 +7,7 @@ lastUpdated: 30th June 2023
 
 Smart contracts, though most are relatively simple, are prone to bugs like any program. However, within the context of a blockchain, it can be hard for a developer to predict and test for all the interactions and externalities possible. As a consequence, this can lead to critical bugs which can and has led to the loss of funds.
 
-One of the great benefits of Tezos is the ability to formally verify smart contracts. Tezos makes this formal verification possible for smart contracts with the design of Michelson and with tools such as [Coq](/developers/docs/advanced-topics/formal-verification/coq/) and the [Mi-Cho-Coq library](/developers/docs/advanced-topics/formal-verification/michocoq).
+One of the great benefits of Tezos is the ability to formally verify smart contracts. Tezos makes this formal verification possible for smart contracts with the design of Michelson and with tools such as [Coq](/advanced-topics/formal-verification/coq/) and the [Mi-Cho-Coq library](/advanced-topics/formal-verification/michocoq).
 
 ## Trust & Formal Verification
 
@@ -26,7 +26,7 @@ The formal verification process on Tezos for smart contracts consists of:
 
 ### How does Tezos make Formal Verification possible?
 
-The [Michelson](/developers/docs/smart-contracts/smart-contract-languages/michelson/) language has been designed to take formal verification into account:
+The [Michelson](/smart-contracts/smart-contract-languages/michelson/) language has been designed to take formal verification into account:
 
 - introducing a typing system on a stack-based language
 - preventing JUMP instructions which would make the formal verification more complex
@@ -45,24 +45,24 @@ Generally speaking, smart contracts also have specific characteristics making th
 
 There are many proof assistants available to translate a smart contract into a formal definition, formalize its specifications and ensure its compliance with these specifications:
 
-- [Coq](/developers/docs/advanced-topics/formal-verification/coq/) is a proof assistant designed to develop mathematical proofs, and especially to write formal specifications, programs, and proofs that programs comply to their specifications.
+- [Coq](/advanced-topics/formal-verification/coq/) is a proof assistant designed to develop mathematical proofs, and especially to write formal specifications, programs, and proofs that programs comply to their specifications.
     - The specification of a program represents **what** a program is meant to do. _Coq_ provides a language [Gallina](https://en.wikipedia.org/wiki/Coq#Overview) for modelling logical objects such as theorems, axioms and assumptions. The proof is a sequence of logical deductions (based on axioms, assumptions and the inference rule) that verify the **compliance of a program to its specification**.
 
-- [Mi-Cho-Coq](/developers/docs/advanced-topics/formal-verification/michocoq), a library which bridges between Tezos smart contracts and formal proofs in the [Coq](/developers/docs/advanced-topics/formal-verification/coq/) proof assistant.
+- [Mi-Cho-Coq](/advanced-topics/formal-verification/michocoq), a library which bridges between Tezos smart contracts and formal proofs in the [Coq](/advanced-topics/formal-verification/coq/) proof assistant.
 
 - [K-Michelson](https://runtimeverification.github.io/michelson-semantics/) is based on K-framework which is a generic tool for specifications and proof languages.
 
 ### Mi-Cho-Coq
 
 {% callout type="note" title="Further Reading" %}
-If you want a deeper introduction to using Mi-Cho-Coq, please see our page on [Mi-Cho-Coq](/developers/docs/advanced-topics/formal-verification/michocoq). The official repository can be found [here](https://gitlab.com/nomadic-labs/mi-cho-coq).
+If you want a deeper introduction to using Mi-Cho-Coq, please see our page on [Mi-Cho-Coq](/advanced-topics/formal-verification/michocoq). The official repository can be found [here](https://gitlab.com/nomadic-labs/mi-cho-coq).
 {% /callout %}
 
 Coq, combined with Mi-Cho-Coq library, provides a manual low-level approach to manually write a proof. This approach performs verification at the smart contract level (i.e. the Michelson script). It also provides a way to perform formal verification on smart contracts written in high-level languages (LIGO, SmartPy) since ultimately they are compiled to Michelson.
 
-The Mi-Cho-Coq library represents the bridge between Tezos smart contracts and formal proofs in Coq. It is a formalization of the Michelson language using the Coq interactive theorem prover. In practice, the Mi-Cho-Coq library is used to produce a formal definition of a Michelson script (known as the the [modelling theorem](/developers/docs/advanced-topics/formal-verification/modelling-theorem/#modelling-a-smart-contract-as-a-theorem)). Each Michelson instruction has its equivalent in the Mi-Cho-Coq library.
+The Mi-Cho-Coq library represents the bridge between Tezos smart contracts and formal proofs in Coq. It is a formalization of the Michelson language using the Coq interactive theorem prover. In practice, the Mi-Cho-Coq library is used to produce a formal definition of a Michelson script (known as the the [modelling theorem](/advanced-topics/formal-verification/modelling-theorem/#modelling-a-smart-contract-as-a-theorem)). Each Michelson instruction has its equivalent in the Mi-Cho-Coq library.
 
-Specifically, the Mi-Cho-Coq library provides a formal definition (in *Gallina*) of the **type system** (Michelson types), the **syntax** (instructions of the Michelson), the **semantics** (evaluator) and the lexing and parsing (for type-checking) (see [Mi-Cho-Coq](/developers/docs/advanced-topics/formal-verification/michocoq)).
+Specifically, the Mi-Cho-Coq library provides a formal definition (in *Gallina*) of the **type system** (Michelson types), the **syntax** (instructions of the Michelson), the **semantics** (evaluator) and the lexing and parsing (for type-checking) (see [Mi-Cho-Coq](/advanced-topics/formal-verification/michocoq)).
 
 There are several considerations to take into account when thinking about using Mi-Cho-Coq:
 - data serialization/deserialization is not supported yet

src/pages/advanced-topics/formal-verification/introduction/index.md

@@ -6,27 +6,27 @@ authors: Frank Hillard
 lastUpdated: 30th June 2023
 ---
 
-One of the great benefits of Tezos is the ability to formally verify smart contracts. Tezos makes this formal verification possible for smart contracts with the design of Michelson and with tools such as [Coq](/developers/docs/advanced-topics/formal-verification/coq/) and the [Mi-Cho-Coq library](/developers/docs/advanced-topics/formal-verification/michocoq).
+One of the great benefits of Tezos is the ability to formally verify smart contracts. Tezos makes this formal verification possible for smart contracts with the design of Michelson and with tools such as [Coq](/advanced-topics/formal-verification/coq/) and the [Mi-Cho-Coq library](/advanced-topics/formal-verification/michocoq).
 
 This entire section walks through formal verification and how it relates to Tezos:
 
-- [Formal Verification on Tezos](/developers/docs/advanced-topics/formal-verification/formal-verification-on-tezos/) discusses how smart contracts on Tezos can be formally verified, its benefits, and what tooling makes this possible.
+- [Formal Verification on Tezos](/advanced-topics/formal-verification/formal-verification-on-tezos/) discusses how smart contracts on Tezos can be formally verified, its benefits, and what tooling makes this possible.
 
-- [Modelling for Smart Contracts](/developers/docs/advanced-topics/formal-verification/modelling-theorem/) goes through an example smart contract, its formal specification and its proof.
+- [Modelling for Smart Contracts](/advanced-topics/formal-verification/modelling-theorem/) goes through an example smart contract, its formal specification and its proof.
 
-- [Coq](/developers/docs/advanced-topics/formal-verification/coq/) gives a brief introduction to syntax and proof creating on Tezos using Mi-Cho-Coq.
+- [Coq](/advanced-topics/formal-verification/coq/) gives a brief introduction to syntax and proof creating on Tezos using Mi-Cho-Coq.
 
-- [Mi-Cho-Coq](/developers/docs/advanced-topics/formal-verification/michocoq/) discusses what Mi-Cho-Coq is and how it bridges between Tezos smart contracts and formal proofs in Coq.
+- [Mi-Cho-Coq](/advanced-topics/formal-verification/michocoq/) discusses what Mi-Cho-Coq is and how it bridges between Tezos smart contracts and formal proofs in Coq.
 
 
 ## Visual Overview
 
 The image below helps visualise the process for performing formal verification for Tezos smart contracts:
 
-![](/developers/docs/images/introduction/FormalVerification_overview_intro.svg)
+![](images/introduction/FormalVerification_overview_intro.svg)
 
 {% callout type="note" title="Further Reading" %}
-For mathematicians and very curious developers, an extra [theoretical](/developers/docs/advanced-topics/formal-verification/gadt-coq) section will introduce some basic concepts of **Type theory** such as *GADT* which allows inductive types on the Calculus of Inductive Construction (CiC). The proof assistant Coq, which is based on the CiC, can be used for proving theorems. 
+For mathematicians and very curious developers, an extra [theoretical](/advanced-topics/formal-verification/gadt-coq) section will introduce some basic concepts of **Type theory** such as *GADT* which allows inductive types on the Calculus of Inductive Construction (CiC). The proof assistant Coq, which is based on the CiC, can be used for proving theorems. 
 {% /callout %}
 
 

src/pages/advanced-topics/formal-verification/modelling-theorem/index.md

@@ -5,18 +5,18 @@ authors: Frank Hillard (Cardashift)
 lastUpdated: 30th June 2023
 ---
 
-This section describes how to bridge Tezos and the [Michelson](/developers/docs/smart-contracts/smart-contract-languages/michelson/) language with the formal world of [Coq](/developers/docs/advanced-topics/formal-verification/coq/). To achieve this, we are going to model a theorem representing a smart contract and the goal of the smart contract.
+This section describes how to bridge Tezos and the [Michelson](/smart-contracts/smart-contract-languages/michelson/) language with the formal world of [Coq](/advanced-topics/formal-verification/coq/). To achieve this, we are going to model a theorem representing a smart contract and the goal of the smart contract.
 
 ## Overview
-The Tezos blockchain can run smart contracts using the Michelson language. Michelson is a low-level stack-based Turing-complete language that is formally proven. The proof of Michelson language is compiled in a library called [Mi-Cho-Coq](/developers/docs/advanced-topics/formal-verification/michocoq/).
+The Tezos blockchain can run smart contracts using the Michelson language. Michelson is a low-level stack-based Turing-complete language that is formally proven. The proof of Michelson language is compiled in a library called [Mi-Cho-Coq](/advanced-topics/formal-verification/michocoq/).
 
 The Coq proof assistant is built upon the paradigm of **calculus of constructions**. The [Gallina](https://en.wikipedia.org/wiki/Coq#Overview) language provides a syntax (terms) for describing formal objects (a theorem) and also provides a set of instructions (vernacular syntax, know as tactics) for writing the proof of the theorem.
 
 The formal verification of a Michelson smart contract is done by providing the proof for this theorem. Coq will perform the verification of a given proof (and its related theorem) based on the Mi-Cho-Coq proof.
 
 The proof consists in a sequence of tactics which the Coq engine will interpret. These instructions manipulate formal expressions (following laws of logic and the Mi-Cho-Coq definitions) to formally assert the truth of a given theorem (based on the given assumptions).
 
-![](/developers/docs/images/modelling-theorem/overview_process.svg)
+![](/images/modelling-theorem/overview_process.svg)
 
 Notice that Gallina provides:
 
@@ -33,18 +33,18 @@ The modelling theorem is based on:
 
 Formal verification of a Tezos smart contract consists in verifying formally that **the execution of the Michelson script satisfies specific post-conditions**.
 
-![](/developers/docs/images/modelling-theorem/overview_theorem.svg)
+![](/images/modelling-theorem/overview_theorem.svg)
 
 The schema above describes an equivalence between the execution of instructions and post-conditions (A, B, C, D). Post-conditions are rules that must be verified, but these post-conditions do not describe the whole behaviour of the smart contract, only specific traits representing the intent of the smart contract.
 
 In the following sections, we will detail how the execution of a Michelson script can be formally written and how to define the post-conditions. We will then study the formal proof as a sequence of Coq tactics (i.e. the vernacular part of the Gallina language).
 
 ### Smart Contract Invocation
-Tezos smart contracts can be written in multiple high-level [languages](/developers/docs/smart-contracts/smart-contract-languages/) but these are all ultimately compiled in Michelson.
+Tezos smart contracts can be written in multiple high-level [languages](/smart-contracts/smart-contract-languages/) but these are all ultimately compiled in Michelson.
 
 A smart contract invocation requires the smart contract itself (through its address), the entrypoint that is being called (and its related arguments) and the storage state. If all these elements are provided, the execution of the smart contract code is triggered, which results in side-effects on storage and optionally on the Tezos network itself:
 
-![](/developers/docs/images/modelling-theorem/smartcontract_invocation.svg)
+![](/images/modelling-theorem/smartcontract_invocation.svg)
 
 The entrypoint information is used to identify which portion of the code will be executed. The entrypoint arguments and the storage are used as the context of execution (i.e, the execution stack is initialized with arguments and a storage). The execution of the code produces a new storage state and operations.
 The operations produced by this invocation are also some new invocations of other smart contracts.
@@ -168,7 +168,7 @@ End ST.
 
 ### Annotated Script
 
-The smart contract is a Michelson script but this script cannot be taken as input by the Coq engine as is. [Mi-Cho-Coq](/developers/docs/advanced-topics/formal-verification/michocoq/) (the Coq specification of the Michelson language) provides the correspondence between a Michelson instruction and an equivalent logical proposition. There is no automated process that translates Michelson code into a formal definition based on Mi-Cho-Coq definitions. Therefore, this must be done manually.
+The smart contract is a Michelson script but this script cannot be taken as input by the Coq engine as is. [Mi-Cho-Coq](/advanced-topics/formal-verification/michocoq/) (the Coq specification of the Michelson language) provides the correspondence between a Michelson instruction and an equivalent logical proposition. There is no automated process that translates Michelson code into a formal definition based on Mi-Cho-Coq definitions. Therefore, this must be done manually.
 
 The example voting smart contract can be formalized in a formal definition in Coq (_Terms_ part of the _Gallina_ language):
 
@@ -212,7 +212,7 @@ Now, these rules can be translated into formal propositions. These propositions
 
 The post conditions of the example contract can be visualised:  
 
-![](/developers/docs/images/modelling-theorem/postconditions_rules.svg)
+![](/images/modelling-theorem/postconditions_rules.svg)
 
 The rule "Keys of the old storage exists in the new storage" can be written in Coq (Gallina - Terms) with the following:
 
@@ -318,7 +318,7 @@ eval env CODE fuel (arguments, storage) = return (newStorage) <=> post-condition
 
 Here is a schema describing graphically the theorem formalization:
 
-![](/developers/docs/images/modelling-theorem/theorem_graphical.svg)
+![](/images/modelling-theorem/theorem_graphical.svg)
 
 Now that we have defined the post-conditions to verify, we can define the theorem in Gallina (Terms) syntax: 
 
@@ -338,7 +338,7 @@ The `vote` object represents our smart contract (in a formal representation). No
 
 We can represent this equivalence between the execution of the code and the verification of post-conditions by the following diagram:
 
-![](/developers/docs/images/modelling-theorem/theorem_graphical_detail.svg)
+![](/images/modelling-theorem/theorem_graphical_detail.svg)
 
 Notice that the `vote_spec` definition is used as post condition and requires 4 arguments (`storage`, `param`, `new_storage`, `returned_operations`). 
 

src/pages/advanced-topics/smart-rollups/index.md

@@ -9,7 +9,7 @@ Rollups play a crucial part in providing next-generation scaling on Tezos. This
 
 ## Prerequisites
 
-This page covers an advanced topic at the bleeding edge of Tezos core development. If you are interested in more fundamental reading, a great place to start is [Tezos Protocol and Shell](/developers/docs/tezos-basics/tezos-protocol-and-shell/) and [Smart Contracts](/developers/docs/smart-contracts/smart-contract-languages/).
+This page covers an advanced topic at the bleeding edge of Tezos core development. If you are interested in more fundamental reading, a great place to start is [Tezos Protocol and Shell](/tezos-basics/tezos-protocol-and-shell/) and [Smart Contracts](/smart-contracts/smart-contract-languages/).
 
 ## What is a rollup?