Skip to content

Instantly share code, notes, and snippets.

View JoJoDeveloping's full-sized avatar
💭
🦉

Johannes Matthias Hostert JoJoDeveloping

💭
🦉
17 followers · 7 following
  • ETH Zurich
  • Zürich, Switzerland
  • 06:54 (UTC +02:00)
View GitHub Profile
@JoJoDeveloping
JoJoDeveloping / Recursion.v
Last active November 22, 2023 02:48 — forked from Agnishom/Attempt1.v
Convoy Pattern + Sigma Types + Equations
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Require Import Arith.
Import ListNotations.
Require Import Coq.Init.Nat.
Require Import Lia.
@JoJoDeveloping
JoJoDeveloping / UIP_extends.v
Last active June 21, 2023 00:19
A proof that UIP X implies UIP (list X)
From Coq Require Import Arith Lia List.
Definition UIP (T:Type) := forall (x y:T) (H1 H2 : x = y), H1 = H2.
Definition sigma {X:Type} {x y : X} (H : x=y) : y=x := match H in (_=z) return z=x with eq_refl _ => eq_refl end.
Definition tau {X:Type} {x y z: X} (H1 : x=y) : y=z -> x=z := match H1 in (_=w) return w=z->x=z with eq_refl _ => fun H => H end.
(* A hedberg function yields a constant path if both arguments are equal
(i.e. the output path does not depend on the input path)
Usually these are constructed using an equalitiy decider.
@JoJoDeveloping
JoJoDeveloping / ra_eqdec.v
Created November 9, 2022 09:49
Equality-Deciding and enumerating mu-recursive functions.
Require Import Arith Lia List Bool Eqdep_dec EqdepFacts.
From Undecidability.Shared.Libs.DLW
Require Import utils_tac utils_nat utils_list finite pos vec.
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts.
From Undecidability Require Import Shared.ListAutomation Shared.Dec.
From Undecidability Require Import Shared.Libs.PSL.Vectors.Vectors.
Import ListAutomationNotations.
Require Import Undecidability.MuRec.recalg.
@JoJoDeveloping
JoJoDeveloping / generated.v
Last active February 2, 2022 21:34
Unique generator ghost state
From iris.base_logic Require Import invariants.
From iris.base_logic.lib Require Import mono_nat.
From iris.heap_lang Require Import lang primitive_laws notation.
From iris.prelude Require Import options.
From iris.proofmode Require Import tactics.
(* You might need to uncomment resource_algebras in your _CoqMakefile *)
From semantics.axiomatic Require Import invariant_lib ghost_state_lib hoare_lib ra_lib ipm resource_algebras.
From semantics.axiomatic.heap_lang Require Import adequacy proofmode primitive_laws.
From semantics.axiomatic.program_logic Require Import notation.
@JoJoDeveloping
JoJoDeveloping / decomp.log
Last active June 5, 2020 10:28
This file has been truncated, but you can view the full file.
INFO: JVM info: Oracle Corporation - 1.8.0_242 - 25.242-b08
INFO: Adding File to context from classpath: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO: Adding Archive: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO: Loading Class: org/jetbrains/java/decompiler/struct/IDecompiledData.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/StructMember.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine$1.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode$RuleValue.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/IMatchable$MatchProperties.class
@JoJoDeveloping
JoJoDeveloping / decomp.log
Created June 5, 2020 10:25
This file has been truncated, but you can view the full file.
INFO: JVM info: Oracle Corporation - 1.8.0_242 - 25.242-b08
INFO: Adding File to context from classpath: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO: Adding Archive: /mnt/workfs/johannes/Minecraft/Forge/114/MCPConfig/build/libraries/net/minecraftforge/forgeflower/1.5.380.45/forgeflower-1.5.380.45.jar
INFO: Loading Class: org/jetbrains/java/decompiler/struct/IDecompiledData.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/StructMember.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchEngine$1.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/MatchNode$RuleValue.class
INFO: Loading Class: org/jetbrains/java/decompiler/struct/match/IMatchable$MatchProperties.class
@JoJoDeveloping
JoJoDeveloping / all_mc_classes.txt
Created August 27, 2019 12:26
com.mojang.blaze3d.platform.GLX
com.mojang.blaze3d.platform.GLX$FboMode
com.mojang.blaze3d.platform.GlStateManager
com.mojang.blaze3d.platform.GlStateManager$AlphaState
com.mojang.blaze3d.platform.GlStateManager$BlendState
com.mojang.blaze3d.platform.GlStateManager$BooleanState
com.mojang.blaze3d.platform.GlStateManager$ClearState
com.mojang.blaze3d.platform.GlStateManager$Color
com.mojang.blaze3d.platform.GlStateManager$ColorLogicState
com.mojang.blaze3d.platform.GlStateManager$ColorMask
@JoJoDeveloping
JoJoDeveloping / ArbeitJuli18Lösung.pdf
Last active July 15, 2021 15:38
Lösungen für die Klausur "Mathe für Informatiker II" an der Universität des Saarlandes vom Juli 2018. Diese Version wird fortlaufend aktualisiert.
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@JoJoDeveloping
JoJoDeveloping / bash.sh
Created July 23, 2019 23:26
curl -O https://files.minecraftforge.net/maven/de/oceanlabs/mcp/mcp_snapshot/20190723-1.14.3/mcp_snapshot-20190723-1.14.3.zip
curl -O https://files.minecraftforge.net/maven/de/oceanlabs/mcp/mcp_config/1.14.4/mcp_config-1.14.4.zip
unzip mcp_config-1.14.4.zip
unzip mcp_snapshot-20190723-1.14.3.zip
cp config/* .
cp ../../MinecraftForge/projects/mcp/build/mcp/mcinject/output.jar joined_srg.jar
ls
#access.txt exceptions.txt mcp_config-1.14.4.zip patches
#config fields.csv mcp_snapshot-20190723-1.14.3.zip static_methods.txt
#config.json joined_srg.jar methods.csv
@JoJoDeveloping
JoJoDeveloping / build.gradle.diff
Created June 27, 2019 20:37
diff --git a/build.gradle b/build.gradle
index a1bc39dd9..33416efdb 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,6 +1,7 @@
buildscript {
repositories {
mavenLocal()
+ maven { url = 'http://localhost:8000' }
maven { url = 'https://files.minecraftforge.net/maven' }